A Framework for Certified Self-Stabilization

TL;DR

This paper introduces a framework using Coq to certify distributed self-stabilizing algorithms, validated through certifying a clustering algorithm and related properties, enhancing trustworthiness in distributed computing.

Contribution

The paper presents a novel framework for certifying self-stabilizing algorithms in Coq, including a library for potential functions and set cardinality, with practical certification of a clustering algorithm.

Findings

Certified a clustering algorithm's correctness in Coq

Validated a bound on the number of clusterheads

Developed a reusable library for potential functions

Abstract

We propose a general framework to build certified proofs of distributed self-stabilizing algorithms with the proof assistant Coq. We first define in Coq the locally shared memory model with composite atomicity, the most commonly used model in the self-stabilizing area. We then validate our framework by certifying a non trivial part of an existing silent self-stabilizing algorithm which builds a $k$-clustering of the network. We also certify a quantitative property related to the output of this algorithm. Precisely, we show that the computed $k$-clustering contains at most $\lfloor \frac{n-1}{k+1} \rfloor + 1$ clusterheads, where $n$ is the number of nodes in the network. To obtain these results, we also developed a library which contains general tools related to potential functions and cardinality of sets.