|
| 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 Forum |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
| Organisation: |
CONVECS project-team, Inria Grenoble Rhône Alpes and LIG, Grenoble (FRANCE)
|
|---|---|
| Method: |
LNT
MCL |
| Tools used: |
CADP (Construction and Analysis of Distributed Processes)
|
| Domain: |
Distributed Systems
|
| Period: |
2012-2013
|
| Size: |
500,000 states and 1,200,000 transitions
|
| Description: |
Distributed systems are hard to design, and formal methods help to
find bugs early. Yet, there may still remain a semantic gap between
a formal model and the actual distributed implementation, which is
generally hand-written. Automated generation of the distributed
implementation from the (validated) formal model would greatly help
gain confidence in the implemented system.
In formal languages inheriting from process algebras (in particular CSP or LOTOS), synchronization can be multiway, meaning that more than two tasks may synchronize altogether. In this case, the generated implementation requires an elaborate synchronization protocol handling multiway synchronization. This study checks the correctness of three such protocols, proposed in the 90's respectively by Sjodin, Parrow & Sjodin, and Sisto, Ciminiera & Valenzano. LNT models of the protocols are generated automatically for specific system instances, and checked automatically using CADP. |
| Conclusions: |
Thanks to CADP, a bug leading to a deadlock in Parrow & Sjodin's
protocol has been found and corrected. The corrected version of this
protocol could then serve as the basis for an extension to the
extended parallel composition operator of LNT, which supports m-among-n
synchronization, where any subset of m processes among a set of n can
synchronize altogether.
|
| Publications: |
[Evrard-Lang-13]
Hugues Evrard and Frédéric Lang.
"Formal Verification of Distributed Branching Multiway Synchronization
Protocols". Proceedings of the IFIP Joint International Conference on
Formal Techniques for Distributed Systems FORTE/FMOODS'2013 (Florence,
Italy), volume 7892 of Lecture Notes in Computer Science, pages
146-160, Springer-Verlag, June 2013.
Available on-line from: http://cadp.inria.fr/publications/Evrard-Lang-13.html or from: http://hal.inria.fr/hal-00818788/en |
| Contact: | Hugues Evrard Inria Grenoble Rhône Alpes / CONVECS project-team 655, avenue de l'Europe 38330 Montbonnot FRANCE E-mail: Hugues.Evrard@inria.fr |
| Further remarks: | This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies |
Back to the CADP case studies page