Specification and Verification of Various Distributed Leader Election Algorithms for Unidirectional Ring Networks

Hubert Garavel and Laurent Mounier

Science of Computer Programming, volume 29, number 1-2, pages 171-197, July 1997

Full version available as INRIA Research Report RR-2986.

Abstract:

This report 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.

35 pages

PDF

PostScript