INRIA Rhone-Alpes (FRANCE)
CADP (Construction and Analysis of Distributed Processes)
LOTOS description of the Leader election algorithm in a reliable network:
LOTOS description of the Leader election algorithm in an unreliable network, without station crashes: 106 lines
LOTOS description of the Leader election algorithm with station crashes: 128 lines
Distributed leader election algorithms aim at designating a unique
member in a set of stations connected by a network. These algorithms
depend on the topology of the network. In the particular case of
unidirectional ring networks, two famous algorithms have been proposed,
the first one by G. Le Lann [Lan77] and its variant proposed by E. Chang
and R. Roberts [CR79].
We studied these two algorithms and several variants, in various contexts, taking into account message losses and/or station crashes. All these algorithms have been formally described in LOTOS and verified using the CADP toolbox.
We pointed out that the algorithms proposed in [Lan77,CR79] were
not complete and did not guarantee the uniqueness of the elected leader
in a token-passing context where several elections can take place in
We proposed an enhanced version of a leader election algorithm that solves this problem and tolerates message losses and station crashes.
Using model-checking and bisimulation techniques, the verification of these non-trivial algorithms was carried out automatically for a fixed number of stations (three stations) [GM96].
Recently, the use of new compositional verification techniques allowed to verify the proposed fault-tolerant protocol with a larger number of stations (up to five or six stations) [KM97].
655 avenue de l'Europe
38330 Montbonnot Saint Martin
Tel: +(33) 4 76 61 52 24
Fax: +(33) 4 76 61 52 52
E-mail : Hubert.Garavel@inria.fr
2, avenue de Vignate
tel : +(33) 4 76 63 48 52
fax : +(33) 4 76 63 48 50
E-mail : Laurent.Mounier@imag.fr
The LOTOS sources as well as explanations on the verification with CADP
are available on-line at :
This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies