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.

• Type: Conference
• Year: 2001
• Where: GI
• Authors: Dominique Cansell, Dominique Méry, Stephan Merz
• Keywords: GI 2001, Interactive Verification Technology, Non-trivial Verification Task, Theorem Proving, Theoretical Computer Science