Résumé | Joint work with Pierre Corbineau and Stéphane Devismes
Self-stabilization is a property that allows distributed algorithms
to withstand transient faults and recover a correct behavior within
finite time. It has been introduced by Dijkstra in 1974. Over the
last decades, progress in self-stabilization has led to consider
more and more adversarial environments. This make the design, proof
for correctness and complexity analysis of self-stabilizing
solutions more and more intricate.
However, those proofs are commonly written by hand, based on
informal reasoning. In this work, we propose instead to use a proof
assistant, a tool which allows to develop certified proofs
interactively and check them mechanically. We present the PADEC
framework, a Coq library dedicated to building certified proofs of
self-stabilizing algorithms.
We first define in Coq the computational model which is the most
commonly used in the self-stabilizing area, and its semantics. We
propose several tools for proving convergence of algorithms and for
counting elements. We illustrate the use of our framework by:
- certifying a non-trivial part of an existing self-stabilizing
algorithm;
- certifying a commonly-used composition operation for
self-stabilizing algorithms. |