HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
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 Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2006 - 1:35:00 PM
Last modification on : Friday, February 4, 2022 - 3:17:31 AM
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

212

Files downloads

436