Navegar

Colección

Datos Estadísticas

Artículo

Braberman, V.; Garbervetsky, D.; Olivero, A. "Improving the verification of timed systems using influence information" (2002) 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002, Proceedings. 2280 LNCS:21-36
La versión final de este artículo es de uso interno. El editor solo permite incluir en el repositorio el artículo en su versión post-print. Por favor, si usted la posee enviela a
Consulte la política de Acceso Abierto del editor

Abstract:

The parallel composition with observers is a well-known approach to check or test properties over formal models of concurrent and real-time systems. We present a newtechnique to reduce the size of the resulting model. Our approach has been developed for a formalism based on Timed Automata. Firstly, it discovers relevant components and clocks at each location of the observer using influence information. Secondly, it outcomes an abstraction which is equivalent to the original model up to branching-time structure and can be treated by verification tools such as KRONOS [12] or OPENKRONOS [23]. Our experiments suggest that the approach may lead to significant time and space savings during verification phase due to state space reduction and the existence of shorter counterexamples in the optimized model. © Springer-Verlag Berlin Heidelberg 2002.

Registro:

Documento: Artículo
Título:Improving the verification of timed systems using influence information
Autor:Braberman, V.; Garbervetsky, D.; Olivero, A.
Ciudad:Grenoble
Filiación:Computer Science Department, FCEyN, Universidad de Buenos Aires, Argentina
Department of Information Technology, FIyCE, Universidad Argentina de la Empresa, Argentina
Palabras clave:Optimized models; Original model; Parallel composition; Relevant components; State-space reduction; Timed Automata; Timed systems; Verification tools; Algorithms; Automata theory; Real time systems; Time sharing systems; Tools; Information use
Año:2002
Volumen:2280 LNCS
Página de inicio:21
Página de fin:36
Título revista:8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002, Proceedings
Título revista abreviado:Lect. Notes Comput. Sci.
ISSN:03029743
Registro:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v2280LNCS_n_p21_Braberman

Referencias:

  • Alpern, B., Schneider, F., Verifying temporal properties without temporal logic (1989) ACM Trans. Programming Lang. and Systems, 11 (1), pp. 147-167
  • Alur, R., Courcoubetis, C., Dill, D., Model-checking for real-time systems (1993) Information and Computation, 104 (1), pp. 2-34
  • Alur, R., Dill, D., A theory of timed automata (1994) Theoretical Computer Science, 126, pp. 183-235
  • Bengtsson, J., Larsen, K.G., Larsson, F., Pettersson, P., Yi, W., UPPAAL - A tool suite for the automatic verification of real-time systems (1996) Proc. Hybrid Systems III, pp. 232-243. , LNCS 1066
  • Bozga, M., Fernandez, J.-C., Ghirvu, L., Using static analysis to improve automatic test generation (2000) TACAS 2000, , LNCS 1785 March/April
  • Braberman, V., (2000) Modeling and Checking Real-Time System Designs, , Ph.D Thesis, Universidad de Buenos Aires
  • Braberman, V., Garbervetsky, D., Olivero, A., Influence information to improve the verification of timed systems Tech. Report DC-UBA 2001-003
  • Braberman, V., Olivero, A., Extending timed automata for compositional modeling healthy timed systems 2nd Workshop on Models for Timed Critical Systems 2001, , To be published in Electronic Notes in Theoretical Computer Science
  • Braberman, V., Olivero, A., Preserving branching-time structure in timed th systems Argentinian Workshop on Theoretical Computer Science 2001, , 30 JAIIO Proceedings
  • Campos, S., Grumberg, O., Yorav, K., Fady, C., Test sequence generation and model checking using dynamic transition relations Submitted To: Fmcad 2000
  • Clarke, E., Grumberg, O., Peled, D., (2000) Model Checking, , MIT Press, January
  • Daws, C., Olivero, A., Tripakis, S., Yovine, S., The tool KRONOS (1996) Proc. of Hybrid Systems III, pp. 208-219. , LNCS 1066
  • Daws, C., Yovine, S., Reducing the number of clock variables of timed automata (1996) Proc. IEEE RTSS '96, , IEEE Computer Soc. Press
  • De Nicolla, R., Montanari, U., Vaandrager, F., Back and forth bisimulations (1990) Proc. CONCUR '90, pp. 152-165. , Amsterdam, LNCS 458
  • Garbervetsky, D., (2000) Un Método de Reducción para la Composición de Sistemas Tem-porizados, , Master Thesis, Univ. de Buenos Aires
  • Godefroid, P., (1996) Partial-Order Methods for the Verification of Concurrent Systems, , LNCS 1032
  • Gawlick, R., Segala, R., Sogaard-Andersen, J., Lynch, N., Liveness in timed and untimed systems (1994) Proceedings of ICALP, pp. 166-177. , LNCS 820, Springer Verlag
  • (1998) Information and Computation, , Also in March
  • Hatcliff, J., Cobett, J., Dwyer, M., Sokolowski, S., Zheng, H., A formal study of slicing for multi-threaded programs with JVM concurrency primitives (1999) SAS, , LNCS 1694
  • Kang, I., Lee, I., Kim, Y.S., An efficient space generation for the analysis of real-time systems (2000) Trans. on Software Engineering, 26 (5), pp. 453-477. , May
  • Larsen, K.G., Laroussinie, F., CMC: A tool for compositional model-checking of real-time systems (1998) Proc. FORTE-PSTV'98, pp. 439-456. , Kluwer Academic Publishers
  • Sloan, R., Buy, U., Stubborn sets for real-time petri Nets (1997) Form. Methods in Syst. Design, 11 (1), pp. 23-40. , July
  • Tasiran, S., Khatri, S.P., Yovine, S., Brayton, R.K., Sangiovanni-Vincentelli, A., A timed automaton-based method for accurate computation of circuit delay in the presence of cross-talk (1998) FMCAD'98
  • Tripakis, S., (1998) L'Analyse Formelle des Systemès Temporisés en Practique, , Phd. Thesis, Univesité Joseph Fourier, December
  • Wang, F., Efficient and user-friendly verification (2001) Transaction in Computers, , Accepted for Publication, June
  • Yi, W., Real-time behavior of asynchronous agents (1990) Proc. CONCUR'90, , LNCS 458
  • Yovine, S., (1993) Methodes et Outiles pour la Verification Symbolique de Systemes Temporises, , doctoral disertation, Insitut National Polytechnique de Grenoble
  • Yovine, S., Model-checking timed automata (1998) Embedded Systems, , G. Rozemberg and F. Vaandrager eds., LNCS 1494

Citas:

---------- APA ----------
Braberman, V., Garbervetsky, D. & Olivero, A. (2002) . Improving the verification of timed systems using influence information. 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002, Proceedings, 2280 LNCS, 21-36.
Recuperado de https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v2280LNCS_n_p21_Braberman [ ]
---------- CHICAGO ----------
Braberman, V., Garbervetsky, D., Olivero, A. "Improving the verification of timed systems using influence information" . 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002, Proceedings 2280 LNCS (2002) : 21-36.
Recuperado de https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v2280LNCS_n_p21_Braberman [ ]
---------- MLA ----------
Braberman, V., Garbervetsky, D., Olivero, A. "Improving the verification of timed systems using influence information" . 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002, Proceedings, vol. 2280 LNCS, 2002, pp. 21-36.
Recuperado de https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v2280LNCS_n_p21_Braberman [ ]
---------- VANCOUVER ----------
Braberman, V., Garbervetsky, D., Olivero, A. Improving the verification of timed systems using influence information. Lect. Notes Comput. Sci. 2002;2280 LNCS:21-36.
Available from: https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v2280LNCS_n_p21_Braberman [ ]