Database of Research Tools Developed Using CADP

PMC Tool for Compositional Verification Using Partial Model Checking

Organisation: CONVECS project-team, Inria Grenoble Rhône Alpes and LIG, Grenoble (FRANCE)

Functionality: Compositional Verification Using Partial Model Checking

Tools used: CADP (Construction and Analysis of Distributed Processes)

Period: 2012-2013

Description: Partial model checking was proposed by Andersen in 1995 to verify a temporal logic formula compositionally on a composition of processes. It consists in incrementally incorporating into the formula the behavioural information taken from one process - an operation called quotienting - to obtain a new formula that can be verified on a smaller composition from which the incorporated process has been removed. Simplifications of the formula must be applied at each step, so as to maintain the formula at a tractable size.

The PMC tool extends quotienting to the network of labelled transition systems model, which subsumes most parallel composition operators, including m-among-n synchronisation and parallel composition using synchronisation interfaces, available in the E-LOTOS standard. Quotienting is implemented as a simple synchronous product between a graph representation of the formula (called formula graph) and a process, thus enabling quotienting to be implemented efficiently and easily, by reusing existing CADP tools dedicated to graph compositions. Simplifications of the formula are implemented as a combination of bisimulations and reductions using Boolean equation systems applied directly to the formula graph, thus enabling formula simplifications also to be implemented efficiently using the CADP tools.

Conclusions: The implementation of a partial model checker was greatly falicitated by the various software components and tools available in CADP. The partial model checker was experimented in two case-studies, in avionics and in hardware design, possibly leading to huge memory savings (several orders of magnitude) with respect to on-the-fly verification. The implementation of quotienting as a synchronous product also opens the way for combining partial model checking with complementary model generation techniques, such as (compositional) tau-confluence reduction, or restriction using interface constraints.

Publications: [Lang-Mateescu-12] Frédéric Lang and Radu Mateescu. "Partial Model Checking using Networks of Labelled Transition Systems and Boolean Equation Systems". Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS'2012 (Talinn, Estonia), volume of Lecture Notes in Computer Science, Springer-Verlag, March 2012.

Available on-line from:
http://cadp.inria.fr/publications/Lang-Mateescu-12.html
or from:
http://hal.inria.fr/hal-00684471/en

[Lang-Mateescu-13] Frédéric Lang and Radu Mateescu. "Partial Model Checking using Networks of Labelled Transition Systems and Boolean Equation Systems". Logical Methods in Computer Science volume 9, number 4, pages 1-32, October 2013.

Available on-line from:
http://cadp.inria.fr/publications/Lang-Mateescu-13.html
or from:
http://www.lmcs-online.org/ojs/viewarticle.php?id=1241

Contact:
Dr. Frédéric Lang
Inria Grenoble Rhône Alpes / CONVECS project-team
655, avenue de l'Europe
38330 Montbonnot
FRANCE
E-mail: Frederic.Lang@inria.fr

http://convecs.inria.fr/software/pmc/

Further remarks: This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software


Last modified: Tue Sep 8 12:24:29 2015.


Back to the CADP research tools page