Skip to Main content Skip to Navigation
Reports

Specification and Verification of various Distributed Leader Election Algorithm for Unidirectional Ring Networks

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 (CÆSAR/ALDEBARAN) toolbox. Model-checking and bisimulation techniques allow the verification of these non-trivial algorithms to be carried out automatically.
Document type :
Reports
Complete list of metadata

https://hal.inria.fr/inria-00073712
Contributor : Rapport de Recherche Inria <>
Submitted on : Wednesday, May 24, 2006 - 1:35:00 PM
Last modification on : Thursday, February 11, 2021 - 2:56:02 PM
Long-term archiving on: : Sunday, April 4, 2010 - 11:55:48 PM

Identifiers

  • HAL Id : inria-00073712, version 1

Collections

Citation

Hubert Garavel, Laurent Mounier. Specification and Verification of various Distributed Leader Election Algorithm for Unidirectional Ring Networks. [Research Report] RR-2986, INRIA. 1996. ⟨inria-00073712⟩

Share

Metrics

Record views

307

Files downloads

751