Karine Altisen ; Pierre Corbineau ; Stephane Devismes - A Framework for Certified Self-Stabilization

lmcs:2183 - Logical Methods in Computer Science, November 28, 2017, Volume 13, Issue 4 - https://doi.org/10.23638/LMCS-13(4:14)2017
A Framework for Certified Self-Stabilization

Authors: Karine Altisen ; Pierre Corbineau ; Stephane Devismes ORCID-iD

    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.


    Volume: Volume 13, Issue 4
    Published on: November 28, 2017
    Accepted on: November 28, 2017
    Submitted on: October 28, 2016
    Keywords: Computer Science - Distributed, Parallel, and Cluster Computing,Computer Science - Logic in Computer Science
    Fundings :
      Source : OpenAIRE Research Graph
    • Enhancing Safety and Self-Stabilization in Time-Varying Distributed Environments; Funder: French National Research Agency (ANR); Code: ANR-16-CE25-0009

    Linked data

    Source : ScholeXplorer IsReferencedBy DOI 10.1007/978-3-319-49259-9_2
    Source : ScholeXplorer IsReferencedBy DOI 10.1007/s00224-017-9828-z
    • 10.1007/s00224-017-9828-z
    • 10.1007/s00224-017-9828-z
    • 10.1007/978-3-319-49259-9_2
    Synchronous Gathering without Multiplicity Detection: a Certified Algorithm
    Lionel Rieg ; Xavier Urbain ; Xavier Urbain ; Amélie Delga ; Amélie Delga ; Sébastien Tixeuil ; Sébastien Tixeuil ; Thibaut Balabonski ;

    Share

    Consultation statistics

    This page has been seen 506 times.
    This article's PDF has been downloaded 377 times.