CONVECS project-team, Inria Grenoble Rhône Alpes and LIG, Grenoble (FRANCE)
CADP (Construction and Analysis of Distributed Processes)
500,000 states and 1,200,000 transitions
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.
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
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:
Inria Grenoble Rhône Alpes / CONVECS project-team
655, avenue de l'Europe
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|