Formal Analysis of a Self-Stabilizing Algorithm - Using Predicate Diagrams

Dominique Cansell 1 Dominique Méry 1 Stephan Merz
1 MODEL - MODEL (Méthodes formelles et applications)
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We present the verification of a protocol designed to ensure self-stabilization in a ring of processors. The proof is organized as a series of refinements; it is mechanized based on a combination of theorem proving and model checking to guarantee the correctness of these refinements. We argue that the framework of predicate diagrams is flexible enough to carry out a non-trivial verification task, that it provides a natural interface between automatic and interactive verification technology, and that it allows to present the correctness argument in an accessible manner.
Type de document :
Communication dans un congrès
Martin Wirsing. Integrating Diagrammatic and Formal Specification Techniques, 2001, Wien, Austria, pp.39-45, 2001
Liste complète des métadonnées

https://hal.inria.fr/inria-00110548
Contributeur : Publications Loria <>
Soumis le : lundi 30 octobre 2006 - 17:00:08
Dernière modification le : mardi 24 avril 2018 - 13:30:22

Identifiants

  • HAL Id : inria-00110548, version 1

Collections

Citation

Dominique Cansell, Dominique Méry, Stephan Merz. Formal Analysis of a Self-Stabilizing Algorithm - Using Predicate Diagrams. Martin Wirsing. Integrating Diagrammatic and Formal Specification Techniques, 2001, Wien, Austria, pp.39-45, 2001. 〈inria-00110548〉

Partager

Métriques

Consultations de la notice

267