OBSSLICE: A timed automata slicer based on observers

OBSSLICE is an optimization tool suited for the verification of timed automata using virtual 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. OBSSLlCE is fed with a ne...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Braberman, V., Garbervetsky, D., Olivero, A.
Formato: SER
Materias:
Computer aided analysis
Modelling elements
Optimization tools
State-space explosion
Timed Automata
Verification tools
Automata theory
Acceso en línea:http://hdl.handle.net/20.500.12110/paper_03029743_v3114_n_p470_Braberman
Aporte de:
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires
Descripción
Sumario:OBSSLICE is an optimization tool suited for the verification of timed automata using virtual 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. OBSSLlCE 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. © Springer-Verlag Berlin Heidelberg 2004.

Ejemplares similares