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

Detalles Bibliográficos
Autores principales: Braberman, Víctor Adrián, Garbervetsky, Diego
Publicado: 2004
Materias:
Computer aided analysis
Modelling elements
Optimization tools
State-space explosion
Timed Automata
Verification tools
Automata theory
Acceso en línea:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v3114_n_p470_Braberman
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
id paper:paper_03029743_v3114_n_p470_Braberman
record_format dspace
spelling paper:paper_03029743_v3114_n_p470_Braberman2023-06-08T15:28:22Z OBSSLICE: A timed automata slicer based on observers Braberman, Víctor Adrián Garbervetsky, Diego Computer aided analysis Modelling elements Optimization tools State-space explosion Timed Automata Verification tools Automata theory 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. 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. 2004 https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v3114_n_p470_Braberman http://hdl.handle.net/20.500.12110/paper_03029743_v3114_n_p470_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 Computer aided analysis
Modelling elements
Optimization tools
State-space explosion
Timed Automata
Verification tools
Automata theory
spellingShingle Computer aided analysis
Modelling elements
Optimization tools
State-space explosion
Timed Automata
Verification tools
Automata theory
Braberman, Víctor Adrián
Garbervetsky, Diego
OBSSLICE: A timed automata slicer based on observers
topic_facet Computer aided analysis
Modelling elements
Optimization tools
State-space explosion
Timed Automata
Verification tools
Automata theory
description 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.
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 OBSSLICE: A timed automata slicer based on observers
title_short OBSSLICE: A timed automata slicer based on observers
title_full OBSSLICE: A timed automata slicer based on observers
title_fullStr OBSSLICE: A timed automata slicer based on observers
title_full_unstemmed OBSSLICE: A timed automata slicer based on observers
title_sort obsslice: a timed automata slicer based on observers
publishDate 2004
url https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v3114_n_p470_Braberman
http://hdl.handle.net/20.500.12110/paper_03029743_v3114_n_p470_Braberman
work_keys_str_mv AT brabermanvictoradrian obssliceatimedautomataslicerbasedonobservers
AT garbervetskydiego obssliceatimedautomataslicerbasedonobservers
_version_ 1768542738072993792

Ejemplares similares