Database of Case Studies Achieved Using CADP

Verification of Multiway Synchronization Protocols

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


Last modified: Tue Sep 8 09:44:18 2015.


Back to the CADP case studies page