Organisation: 
CONVECS projectteam, 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: 
20122013

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 mamongn synchronisation and parallel composition using synchronisation interfaces, available in the ELOTOS 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 casestudies, in
avionics and in hardware design, possibly leading to huge memory
savings (several orders of magnitude) with respect to onthefly
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)
tauconfluence reduction, or restriction using interface constraints.

Publications: 
[LangMateescu12]
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, SpringerVerlag, March 2012.
Available online from: http://cadp.inria.fr/publications/LangMateescu12.html or from: http://hal.inria.fr/hal00684471/en [LangMateescu13] 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 132, October 2013. Available online from: http://cadp.inria.fr/publications/LangMateescu13.html or from: http://www.lmcsonline.org/ojs/viewarticle.php?id=1241 
Contact:  Dr. Frédéric Lang Inria Grenoble Rhône Alpes / CONVECS projectteam 655, avenue de l'Europe 38330 Montbonnot FRANCE Email: 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 