Abstract:

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.