My
PhD thesis is about algorithmic aspects of parallel formal verification,
more precisely on distributed model-checking approaches.
That is a rather wide subject, isn't it ? :-)
So far, my work can be divided in two parts: distributed verification engine based on Boolean Equation Systems and distributed model-checking applications using the previous engine.
If you want more information, check out the
presentation slide
(513 Kb in french) I made for the MSTII'04 doctoral symposium last december.
You may also consult my list of publications for further information.
Hereafter is a small description of my Ph.D. project:
- place:
- INRIA, Rhône-Alpes research unit, VASY project, Grenoble (France)
- title:
- massively parallel on-the-fly verification of finite-state systems
- domain:
- formal verification methods
- advisors:
- Hubert Garavel (director) and Radu Mateescu (scientific advisor)
- funding:
- french research ministry grant
- project:
- research work part of Standard Process Algebra Research and Tools SENVA, Associated Team INRIA program between INRIA/VASY and CWI/SEN, section distributed algorithms for the verification of finite-state systems
- abstract:
-
The verification of concurrent finite-state systems is confronted in practice with the state explosion problem (prohibitive size of the underlying state spaces), which occurs for realistic systems containing many parallel processes and complex data structures.
Various techniques for fighting against state explosion have been proposed, such as on-the-fly verification, partial order reduction, and distributed verification.
However, practical experience has shown that none of these techniques alone is always sufficient to handle large-scale systems.
In this thesis, we propose a combination of these techniques in order to scale up their capabilities.
Our approach is based upon Boolean Equation Systems (BESs), which provide an elegant intermediate representation for verification problems defined on Labeled Transition Systems (LTSs) such as equivalence checking, tau-confluence reduction, model checking of alternation-free mu-calculus and test-case generation.
We propose DSolve (Joubert - Mateescu - PDP - 05), a new algorithm for distributed on-the-fly resolution of BESs, and employ it as computing engine for four on-the-fly verification tools developed within the CADP toolbox using the OPEN/CAESAR environment: the Bisimulator equivalence checker (Joubert - Mateescu - PDMC - 04, Bergamini - et - al - TACAS - 05 - a), the Tau_Confluence reductor, the Evaluator model checker, and the Extractor test-case generator.
Experimental measures performed on clusters of machines show quasi-linear speedups and a good scalability of the distributed versions of these tools w.r.t. their sequential counterparts.
- keywords:
- boolean equation systems, distributed memory algorithm, on-the-fly verification, equivalence checking, partial order reduction, model checking, test case generation
- publications:
- Bergamini - et - al - TACAS - 05 - a
- Joubert - Mateescu - PDP - 05
- Joubert - Mateescu - PDMC - 04
- Joubert - PDMC - 03
- talks:
- Joubert - MSTII - 04
- Joubert - SENVA - 04
- Joubert - EJCP - 03
- tool demonstration:
- Bergamini - et - al - TACAS - 05 - b