17.06.2004

Mec 5, a model checker for AltaRica models

The AltaRica formalism was developed at the LaBRI in Bordeaux jointly with industrial partners and allows to analyse a given system with several different methods (fault tree, Petri nets, Markov chains) in order to perform safety analysis of the system. This talk is concerned with the model checking of such models, and in particular in the Mec 5 tool which we developed.
We will describe in this talk a few key points of the AltaRica formalism, and then the very expressive specification language we use to compute arbitrary (finite) relations which allow us to express usual "temporal" properties of models as well as e.g. bisimulation relations, in a very natural way. The specification language is first-order logic extended with fixpoints over relations.
We will also give some insight of the implementation of Mec 5 which basically uses binary decision diagrams, and discuss the different ideas we are investigating to improve the performance of Mec 5.