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,...
Guardado en:
| Autores principales: | , , |
|---|---|
| Formato: | SER |
| Materias: | |
| Acceso en línea: | http://hdl.handle.net/20.500.12110/paper_03029743_v2280LNCS_n_p21_Braberman |
| Aporte de: |
| id |
todo:paper_03029743_v2280LNCS_n_p21_Braberman |
|---|---|
| record_format |
dspace |
| spelling |
todo:paper_03029743_v2280LNCS_n_p21_Braberman2023-10-03T15:18:54Z Improving the verification of timed systems using influence information Braberman, V. Garbervetsky, D. Olivero, A. 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. SER info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar 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. Garbervetsky, D. Olivero, A. 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. |
| format |
SER |
| author |
Braberman, V. Garbervetsky, D. Olivero, A. |
| author_facet |
Braberman, V. Garbervetsky, D. Olivero, A. |
| author_sort |
Braberman, V. |
| 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 |
| url |
http://hdl.handle.net/20.500.12110/paper_03029743_v2280LNCS_n_p21_Braberman |
| work_keys_str_mv |
AT brabermanv improvingtheverificationoftimedsystemsusinginfluenceinformation AT garbervetskyd improvingtheverificationoftimedsystemsusinginfluenceinformation AT oliveroa improvingtheverificationoftimedsystemsusinginfluenceinformation |
| _version_ |
1782023642199097344 |