A Mechanically Proved and Incremental Development of IEEE 1394 Tree Identify Protocol

Jean-Raymond Abrial Dominique Cansell 1 Dominique Méry 1
1 MODEL - MODEL (Méthodes formelles et applications)
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : The \ieee tree identify protocol illustrates the adequacy of the \textit{event-driven approach} used together with the B Method . This approach provides a complete framework for developing mathematical models of distributed algorithms. A specific development is made of a series of more and more refined models. Each model is made of a number of static properties (the invariant), and of a dynamic parts (the guarded events). The internal consistency of each model as well as its correctness with regards to its previous abstraction are proved with the proof engine of Atelier B, which is the tool associated with B. In the case of \ieee, the initial model is very primitive: it provides the basic properties of the graph (symmetry, acyclicity, connectivity), and its dynamic parts essentially contains a single event which \textit{elects the leader} in one shot. Further refinements introduce more events, showing how each node of the graph non-deterministically participates to the leader election. At some stage in the development, message passing is introduced. This raises a specific potential contention problem, whose solution is given. The last stage of the refinement completely localize the events by making them taking decision based on local data only.
Type de document :
Article dans une revue
Formal Aspects of Computing, Springer Verlag, 2003, 14 (3), pp.215-227
Liste complète des métadonnées

https://hal.inria.fr/inria-00099531
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 09:38:21
Dernière modification le : mardi 24 avril 2018 - 13:28:57

Identifiants

  • HAL Id : inria-00099531, version 1

Collections

Citation

Jean-Raymond Abrial, Dominique Cansell, Dominique Méry. A Mechanically Proved and Incremental Development of IEEE 1394 Tree Identify Protocol. Formal Aspects of Computing, Springer Verlag, 2003, 14 (3), pp.215-227. 〈inria-00099531〉

Partager

Métriques

Consultations de la notice

230