|Final Report of the COST-247 Action|
Specification in LOTOS and verification of a distributed election algorithm
Hubert Garavel and Laurent Mounier
|INRIA Rhone-Alpes / Dyade|
|655, avenue de l'Europe|
|38330 MONTBONNOT ST MARTIN|
|tel: +(33) 4 76 61 52 24|
|fax: +(33) 4 76 61 52 52|
This talk deals with the formal specification and verification of distributed leader election algorithms for a set of machines connected by a unidirectional ring network. Starting from an algorithm proposed by Le Lann in 1977, and its variant proposed by Chang and Roberts in 1979, we study the robustness of this class of algorithms in presence of unreliable communication medium and/or unreliable machines. We suggest various improvements of these algorithms in order to obtain a fully fault-tolerant protocol. These algorithms are formally described using the ISO specification language LOTOS and verified (for a fixed number of machines) using the CADP (CAESAR/ALDEBARAN) toolbox. Model-checking and bisimulation techniques allow the verification of these non-trivial algorithms to be carried out automatically.
This presentation has been given during the COST-247 6th Management Committee Meeting (Budapest, Hungary, October 26-27, 1995).
COST-247 Working Group(s): 1-2
Web links: http://vasy.inria.fr
This Page was prepared by Mark Jorgensen.