Symbolic Model Checking in Multi-formalism Modelling Environments
Date and Time
Thursday, April 11th, 2013 at 10:30.
Polacksbacken, room 1113
Abstraction in system analysis intends to achieve scalability but maintain correctness in the analysis. High-level (state-based) system modelling techniques allow to abstractly capture essentials of hardware/software systems. With their concrete operational semantics they provide a sound basis for carrying out formal system analysis at an abstract level. Employing different modelling formalism within the same modelling project has the potential to ease the description of various parts or aspects of the overall system. However, the use of different modelling techniques may hamper the use of formalism-dependent analysis techniques and thereby achieve efficiency in the analysis.
This seminar presents an approach for efficiently constructing a symbolic representation of the finite state-to-state transition system of a high-level model. As main feature, the approach is capable of handling high-level models made of components possibly described by different formalisms and where the interaction between components is established either by the sharing of variables or by the synchronisation of common events. Despite this generality, the scheme which relies on (partial) explicit state space traversal targets at the efficient application of any state space based system analysis. As symbolic representation, the talk we will introduce (partially shared) Multi-terminal Zero-suppressed Binary Decision Diagrams.