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)
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
- 2006 activity report of the VASY team
- 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
- 2006 activity report of the VASY team
- 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
- 2006 activity report of the VASY team
- 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.
