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 CÆSAR_SOLVE 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
- Overview publication on OPEN/CAESAR
- article at CAV'2003
- article submitted to FMSD
- 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 tau*.a equivalence checking with BISIMULATOR and BCG graph generation using reachability analysis combined with on-the-fly tau*.a reduction with REDUCTOR.
(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:
- CADP web page
- article at SPIN'2001
- master research report
- 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.
