Speeding up model checking of timed-models by combining scenario specialization and live component analysis

The common practice for verifying properties described as event occurrence patterns is to translate them into observer state machines. The resulting observer is then composed with (the components of) the system under analysis in order to verify a reachability property. Live Component Analysis is a &...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Braberman, V., Garbervestky, D., Kicillof, N., Monteverde, D., Olivero, A.
Formato: SER
Materias:
Abstraction techniques
Component analysis
Distributed real time system
Event pattern
Occurrence pattern
Reachability
State explosion
State machine
Location
Object oriented programming
Real time systems
Time sharing systems
Model checking
Acceso en línea:http://hdl.handle.net/20.500.12110/paper_03029743_v5813LNCS_n_p58_Braberman
Aporte de:
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires
id todo:paper_03029743_v5813LNCS_n_p58_Braberman
record_format dspace
spelling todo:paper_03029743_v5813LNCS_n_p58_Braberman2023-10-03T15:19:12Z Speeding up model checking of timed-models by combining scenario specialization and live component analysis Braberman, V. Garbervestky, D. Kicillof, N. Monteverde, D. Olivero, A. Abstraction techniques Component analysis Distributed real time system Event pattern Occurrence pattern Reachability State explosion State machine Location Object oriented programming Real time systems Time sharing systems Model checking The common practice for verifying properties described as event occurrence patterns is to translate them into observer state machines. The resulting observer is then composed with (the components of) the system under analysis in order to verify a reachability property. Live Component Analysis is a "cone of influence" abstraction technique aiming at mitigating state explosion by detecting, at each observer location, which components are actually relevant for model checking purposes. Interestingly enough, the more locations the observer has, the more precise the relevance analysis becomes. This work proposes the formal underpinnings of a method to safely leverage this fact when properties are stated as event patterns (scenarios). That is, we present a sound and complete method of property manipulation based on specializing and complementing scenarios. The application of this method is illustrated on two case studies of distributed real-time system designs, showing dramatic improvements in the verification phase, even in situations where verification of the original scenario was unfeasible. © 2009 Springer Berlin Heidelberg. Fil:Braberman, V. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. Fil:Kicillof, N. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. Fil:Monteverde, 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_v5813LNCS_n_p58_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 Abstraction techniques
Component analysis
Distributed real time system
Event pattern
Occurrence pattern
Reachability
State explosion
State machine
Location
Object oriented programming
Real time systems
Time sharing systems
Model checking
spellingShingle Abstraction techniques
Component analysis
Distributed real time system
Event pattern
Occurrence pattern
Reachability
State explosion
State machine
Location
Object oriented programming
Real time systems
Time sharing systems
Model checking
Braberman, V.
Garbervestky, D.
Kicillof, N.
Monteverde, D.
Olivero, A.
Speeding up model checking of timed-models by combining scenario specialization and live component analysis
topic_facet Abstraction techniques
Component analysis
Distributed real time system
Event pattern
Occurrence pattern
Reachability
State explosion
State machine
Location
Object oriented programming
Real time systems
Time sharing systems
Model checking
description The common practice for verifying properties described as event occurrence patterns is to translate them into observer state machines. The resulting observer is then composed with (the components of) the system under analysis in order to verify a reachability property. Live Component Analysis is a "cone of influence" abstraction technique aiming at mitigating state explosion by detecting, at each observer location, which components are actually relevant for model checking purposes. Interestingly enough, the more locations the observer has, the more precise the relevance analysis becomes. This work proposes the formal underpinnings of a method to safely leverage this fact when properties are stated as event patterns (scenarios). That is, we present a sound and complete method of property manipulation based on specializing and complementing scenarios. The application of this method is illustrated on two case studies of distributed real-time system designs, showing dramatic improvements in the verification phase, even in situations where verification of the original scenario was unfeasible. © 2009 Springer Berlin Heidelberg.
format SER
author Braberman, V.
Garbervestky, D.
Kicillof, N.
Monteverde, D.
Olivero, A.
author_facet Braberman, V.
Garbervestky, D.
Kicillof, N.
Monteverde, D.
Olivero, A.
author_sort Braberman, V.
title Speeding up model checking of timed-models by combining scenario specialization and live component analysis
title_short Speeding up model checking of timed-models by combining scenario specialization and live component analysis
title_full Speeding up model checking of timed-models by combining scenario specialization and live component analysis
title_fullStr Speeding up model checking of timed-models by combining scenario specialization and live component analysis
title_full_unstemmed Speeding up model checking of timed-models by combining scenario specialization and live component analysis
title_sort speeding up model checking of timed-models by combining scenario specialization and live component analysis
url http://hdl.handle.net/20.500.12110/paper_03029743_v5813LNCS_n_p58_Braberman
work_keys_str_mv AT brabermanv speedingupmodelcheckingoftimedmodelsbycombiningscenariospecializationandlivecomponentanalysis
AT garbervestkyd speedingupmodelcheckingoftimedmodelsbycombiningscenariospecializationandlivecomponentanalysis
AT kicillofn speedingupmodelcheckingoftimedmodelsbycombiningscenariospecializationandlivecomponentanalysis
AT monteverded speedingupmodelcheckingoftimedmodelsbycombiningscenariospecializationandlivecomponentanalysis
AT oliveroa speedingupmodelcheckingoftimedmodelsbycombiningscenariospecializationandlivecomponentanalysis
_version_ 1807322285239959552

Ejemplares similares