| Organisation: |
INRIA Rhone-Alpes (FRANCE)
|
| Method: |
LOTOS
|
| Tools used: |
CADP (Construction and Analysis of Distributed Processes)
|
| Domain: |
Distributed algorithms
|
| Period: |
1996.
|
| Size: |
LOTOS description of the Leader election algorithm in a reliable network:
100 lines
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
|
| Description: |
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.
|
| Conclusions: |
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
sequence.
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) [KM97].
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) [GM96].
|
| Publications: |
- [Lan77]
- Gerard Le Lann. "Distributed Systems - Towards a Formal Approach".
In B. Gilchrist, editor, Information Processing 77, pages 155-160.
IFIP, North Holland, 1977.
- [CR79]
- Ernest Chang and Rosemary Roberts. "An Improved Algorithm for
Decentralized Extrema-Finding in Circular Configurations of Processes".
Communications of the ACM 22(5): 281-283, may 1979.
- [GM96]
- Hubert Garavel and Laurent Mounier. "Specification and verification of
various distributed leader election algorithms for unidirectional ring
networks". Science of Computer Programming, 1996. Special issue on
Industrially Relevant Applications of Formal Analysis Techniques.
Full version available as INRIA Research Report RR-2986.
Available on-line from the VASY FTP site in :
PDF
or
PostScript 
- [KM97]
- Jean-Pierre Krimm and Laurent Mounier. "Compositional state space
generation from lotos programs". In Ed Brinksma, editor, Proceedings of
TACAS'97 (Tools and Algorithms for the Construction and Analysis of
Systems), Enschede, The Netherlands, April 1997. Springer Verlag.
Extended version with proofs available as Research Report VERIMAG
RR97-01. Available on-line from the VASY FTP site in
PDF
or
PostScript
|
| Contact: |
Hubert Garavel
INRIA Rhone-Alpes
655 avenue de l'Europe
38330 Montbonnot Saint Martin
FRANCE
Tel: +(33) 4 76 61 52 24
Fax: +(33) 4 76 61 52 52
E-mail : Hubert.Garavel@inria.fr
-
Laurent Mounier
VERIMAG
Centre Equation
2, avenue de Vignate
F-38610 Gieres
FRANCE
tel : +(33) 4 76 63 48 52
fax : +(33) 4 76 63 48 50
E-mail : Laurent.Mounier@imag.fr
|
| Further remarks: |
The LOTOS sources as well as explanations on the verification with CADP
are available on-line at :
ftp://ftp.inrialpes.fr/pub/vasy/demos/demo_17
This case-study, amongst others, is described on the CADP Web Page :
http://cadp.inria.fr
|
Back to the CADP case studies page