INVESTIGADORES
BRABERMAN Victor Adrian
artículos
Título:
Improving the Verification of Time Systems Using Influence Information
Autor/es:
VICTOR A. BRABERMAN; DIEGO GARBERVETSKY; ALFREDO OLIVERO
Revista:
LECTURE NOTES IN COMPUTER SCIENCE
Editorial:
Springer Verlag
Referencias:
Lugar: Berlin; Año: 2002 vol. 2280 p. 21 - 36
ISSN:
0302-9743
Resumen:
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 new technique 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.
