INVESTIGADORES
BRABERMAN Victor Adrian
artículos
Título:
A Time Automata Slicer Based on Observers
Autor/es:
VICTOR A. BRABERMAN; DIEGO GARBERVETSKY; ALFREDO OLIVERO
Revista:
LECTURE NOTES IN COMPUTER SCIENCE
Editorial:
Springer-Verlag
Referencias:
Lugar: Berlin; Año: 2004 vol. 3114 p. 470 - 474
ISSN:
0302-9743
Resumen:
ObsSlice is an optimization tool suited for the verification of timed automata using virtua observers. It discovers the set of modelling elements that can be safely ignored at each location of the observer by synthesizing behavioral dependence information among components. ObsSlice is fed with a network of timed automata and generates a transformed network which is equivalent to the one provided up to branching-time observation. Preliminary results have proven that eliminating irrelevant activity mitigates state space explosion and has a positive and sometimes dramatic- impact on the performance of verification tools in terms of time, size and counterexample length.
