I've been developping quite a few softwares since I'm part of the Validation of Systems (VASY) project at Rhône-Alpes research unit of INRIA, back in July 2000. Since then, I have been participating to the development of the Construction and Analysis of Distributed Processes (CADP) toolbox.
(top)
ANNOTATOR is a modular tool for on-the-fly data flow analysis of abstract control flow graphs, based on the OPEN/CAESAR environment part of CADP
- Contribution:
- ANNOTATOR provides 8 different data flow analyses ranging from live variables analysis to influence analysis, which take as input an implicit labeled transition system describing the control flow graph of a program to analyse. The tool can be used for state space reduction as it allows to detect which program variables or expressions are necessary in each program control point, and consequently to minimize the state vector used during verification.
- Documentation:
- manual of ANNOTATOR
- Article at ISOLA'2006 on implementing influence analysis using parameterised BESs
- Technical report on static analysis using parameterised boolean equation systems
- Demo examples:
- Numerous ANNOTATOR examples are detailed on the GISUM's software model checking web page
(top)
TAU_CONFLUENCE is an on-the-fly partial order reductor based on OPEN/CAESAR environment part of CADP
- Contribution:
- TAU_CONFLUENCE consists in identifying, for each state s, the set C(s) of confluent tau-transitions going out of s, meaning that after their execution any other transition going out of s can still be executed. The reduction consists in eliminating all transitions going out of s except those in C(s). This tool encodes the definition of tau-confluence as a boolean equation system, which is solved on the fly using the general algorithms A1 and A2 provided by the "solve_1" library. I have participated to the connection of the front-end of TAU_CONFLUENCE with the "solve_2" back-end through the use of one of the distributed algorithms I designed and implemented.
- Documentation:
- CADP web page and Pace-Lang-Mateescu-03, which is the article of reference on TAU_CONFLUENCE
- Overview publication on OPEN/CAESAR
- Papers about equivalence checking using BISIMULATOR and REDUCTOR
- 2005 activity report of the VASY team
- 2004 activity report of the VASY team
- 2003 activity report of the VASY team
- Demo examples:
- The TAU_CONFLUENCE module has successfully been used by other tools of the CADP toolbox, namely for equivalence checking with BISIMULATOR and BCG graph generation using reachability analysis combined with on-the-fly reduction with REDUCTOR.
(top)
available soon ...
EXTRACTOR is an on-the-fly test case generator, based on the OPEN/CAESAR environment part of CADP
- Contribution:
-
Along the lines of the test generation theory implemented in the TGV tool of CADP, we developed a prototype tool named EXTRACTOR that takes as inputs both a ``specification'' graph (represented implicitly using the OPEN/CÆSAR environment) and a ``test purpose'' (represented explicitly as a BCG graph), and computes the ``complete test graph'' (CTG) containing all sequences of observable actions and quiescence present in the specification and allowed by the test purpose. The CTG produced by EXTRACTOR is subsequently processed using the DETERMINATOR tool of CADP to eliminate nondeterminism and tau-transitions. Compared to TGV, EXTRACTOR uses a radically different approach, as it reformulates the CTG generation problem in terms of a boolean equation system, for which a diagnostic is computed using the CÆSAR_SOLVE library.
-
We developed two versions of EXTRACTOR, a sequential one (1, 200 lines of C code) based on the sequential resolution algorithms of CÆSAR_SOLVE, and a distributed one (1, 300 lines of C code) based on the distributed version of CÆSAR_SOLVE. Experiments were performed on various graphs (taken from the VLTS benchmark suite and the CADP demo examples) by using generic test purposes expressing the reachability of certain visible actions. All CTGs obtained by applying EXTRACTOR and DETERMINATOR were strongly equivalent to those produced by TGV, although slightly larger. On some examples, however, the generation of the CTG succeeded using EXTRACTOR and DETERMINATOR, whereas TGV would fail because of memory shortage. These results have been accepted for publication at SPIN'2006.
- Documentation:
- CADP web page
- article at SPIN'2006
- 2005 activity report of the VASY team
(top)
DISTRIBUTOR is a state space generator, part of CADP, using distributed reachability analysis
- Contribution:
- I first worked on DISTRIBUTOR back in 2002 during my master in computer science. I contributed to the correction of version V2.0 of DISTRIBUTOR before redesigning the algorithm (order of distributed tasks, priority between computation and communication, distributed termination detection, protocol of distributed dynamic data structures coherency) which has been integrated in current version (V3.0) of DISTRIBUTOR.
- Documentation:
- my master research report!
- CADP web page
- article at TACAS'2006
- article at SPIN'2001
- Papers about distributed state space generation
- 2005 activity report of the VASY team
- 2004 activity report of the VASY team
- 2003 activity report of the VASY team
- 2002 activity report of the VASY team
- 2001 activity report of the VASY team
- 2000 activity report of the VASY team
- 1999 activity report of the VASY team
- Demo examples:
- from demo_02 available from the CADP online demo examples web page, you can make use of DISTRIBUTOR by constructing a .gcf file that contain the following example lines:
- localhost
- directory=/tmp/A
- localhost
- directory=/tmp/B
- localhost
- directory=/tmp/C
- this specifies a network of three processes (in the parallel.gcf above example, all processes are local to the same machine (user local machine)), and three different working directories (one for each process). Then, by running the following command line:
- caesar.open bitalt_protocol.lotos distributor.a -monitor parallel.gcf bitalt_protocol.pbg
- you'll distribute the generation of alternating bit protocol with 4 messages, over three processes. Once the generation is done, you can merge the partitioned LTS into one LTS by using the BCG_MERGE tool simply as following:
- bcg_merge bitalt_protocol.pbg
- That's it! You've got your final merged generated LTS of the alternating bit protocol with 4 different messages.
- There will be soon more demo examples of DISTRIBUTOR on the CADP online demo examples web page.