Sciweavers

GI
2001
Springer

Formal Analysis of a Self-Stabilizing Algorithm Using Predicate Diagrams

13 years 8 months ago
Formal Analysis of a Self-Stabilizing Algorithm Using Predicate Diagrams
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.
Dominique Cansell, Dominique Méry, Stephan
Added 28 Jul 2010
Updated 28 Jul 2010
Type Conference
Year 2001
Where GI
Authors Dominique Cansell, Dominique Méry, Stephan Merz
Comments (0)