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.
Type de document :
Rapport
[Research Report] RR-2986, INRIA. 1996
Liste complète des métadonnées

https://hal.inria.fr/inria-00073712
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 13:35:00
Dernière modification le : samedi 17 septembre 2016 - 01:27:35
Document(s) archivé(s) le : dimanche 4 avril 2010 - 23:55:48

Fichiers

Identifiants

  • 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〉

Partager

Métriques

Consultations de la notice

161

Téléchargements de fichiers

340