Improving the verification of timed systems using influence information

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,...

Descripción completa

Guardado en:

Detalles Bibliográficos
Autores principales:	Braberman, Víctor Adrián, Garbervetsky, Diego
Publicado:	2002
Materias:	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
Acceso en línea:	https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v2280LNCS_n_p21_Braberman http://hdl.handle.net/20.500.12110/paper_03029743_v2280LNCS_n_p21_Braberman
Aporte de:	Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires

id	paper:paper_03029743_v2280LNCS_n_p21_Braberman
record_format	dspace
spelling	paper:paper_03029743_v2280LNCS_n_p21_Braberman2023-06-08T15:28:21Z Improving the verification of timed systems using influence information Braberman, Víctor Adrián Garbervetsky, Diego 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 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. Fil:Braberman, V. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. Fil:Garbervetsky, D. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. 2002 https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v2280LNCS_n_p21_Braberman http://hdl.handle.net/20.500.12110/paper_03029743_v2280LNCS_n_p21_Braberman
institution	Universidad de Buenos Aires
institution_str	I-28
repository_str	R-134
collection	Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
topic	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
spellingShingle	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 Braberman, Víctor Adrián Garbervetsky, Diego Improving the verification of timed systems using influence information
topic_facet	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
description	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.
author	Braberman, Víctor Adrián Garbervetsky, Diego
author_facet	Braberman, Víctor Adrián Garbervetsky, Diego
author_sort	Braberman, Víctor Adrián
title	Improving the verification of timed systems using influence information
title_short	Improving the verification of timed systems using influence information
title_full	Improving the verification of timed systems using influence information
title_fullStr	Improving the verification of timed systems using influence information
title_full_unstemmed	Improving the verification of timed systems using influence information
title_sort	improving the verification of timed systems using influence information
publishDate	2002
url	https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v2280LNCS_n_p21_Braberman http://hdl.handle.net/20.500.12110/paper_03029743_v2280LNCS_n_p21_Braberman
work_keys_str_mv	AT brabermanvictoradrian improvingtheverificationoftimedsystemsusinginfluenceinformation AT garbervetskydiego improvingtheverificationoftimedsystemsusinginfluenceinformation
_version_	1768546066999803904

Improving the verification of timed systems using influence information

Ejemplares similares