Speeding Up Model Checking of Timed-Models by Combining Scenario Specialization and Live Component Analysis

VICTOR A. BRABERMAN; DIEGO GARBERVETSKY; NICOLAS KICILLOF; DANIEL MONTEVERDE; ALFREDO OLIVERO

Budapest

Conferencia; The 7th International Conference on Formal Modelling and Analysis of Timed Systems; 2009

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 inuence" 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 veri_cation phase, even in situations where verification of the original scenario was unfeasible.