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
id todo:paper_03029743_v3114_n_p470_Braberman
record_format dspace
spelling todo:paper_03029743_v3114_n_p470_Braberman2023-10-03T15:18:55Z OBSSLICE: A timed automata slicer based on observers Braberman, V. Garbervetsky, D. Olivero, A. 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. SER info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar 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.
Garbervetsky, D.
Olivero, A.
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.
format SER
author Braberman, V.
Garbervetsky, D.
Olivero, A.
author_facet Braberman, V.
Garbervetsky, D.
Olivero, A.
author_sort Braberman, V.
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
url http://hdl.handle.net/20.500.12110/paper_03029743_v3114_n_p470_Braberman
work_keys_str_mv AT brabermanv obssliceatimedautomataslicerbasedonobservers
AT garbervetskyd obssliceatimedautomataslicerbasedonobservers
AT oliveroa obssliceatimedautomataslicerbasedonobservers
_version_ 1807322105347309568

Ejemplares similares