|
| What is CADP? |
|---|
|
Home Page
Tools Overview Current Status Recent Changes |
| Installation |
|
How to obtain CADP?
Usage Statistics |
| Documentation |
|
FAQ
Tutorials Publications Manual Pages Demo Examples Wikipedia |
| CADP Community |
|
Newsletters
Education & Training Case Studies Research Tools |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
| 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: [email protected] http://convecs.inria.fr/software/pmc/ |
| Further remarks: | This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software |
Back to the CADP research tools page