Specification and verification of various distributed leader election algorithms for unidirectional ring networks

This paper 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 these algorithms in the presence of unreliable communication medium and unreliable machines. We propose various improvements of these algorithms in order to obtain a fully fault-tolerant protocol