Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata

https://hal.inria.fr/inria-00110548
Contributor : Publications Loria <>
Submitted on : Monday, October 30, 2006 - 5:00:08 PM
Last modification on : Friday, February 26, 2021 - 3:28:08 PM

Identifiers

  • 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. Integrating Diagrammatic and Formal Specification Techniques, GI Fachgruppe 0.1.7 Specification and Semantics, 2001, Wien, Austria, pp.39-45. ⟨inria-00110548⟩

Share

Metrics

Record views

427