Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, EpiSciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
Skip to Main content Skip to Navigation
Conference papers

A Framework for Certified Self-Stabilization

Abstract : We propose a framework to build certified proofs of self-stabilizing algorithms using 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 self-stabilizing algorithm which builds a k-hop dominating set of the network. We also certify a quantitative property related to its output: we show that the size of the computed k-hop dominating set is at most $$\lfloor \frac{n-1}{k+1} \rfloor + 1$$⌊n-1k+1⌋+1, where n is the number of nodes. To obtain these results, we developed a library which contains general tools related to potential functions and cardinality of sets.
Complete list of metadata

Cited literature [18 references]  Display  Hide  Download
Contributor : Hal Ifip Connect in order to contact the contributor
Submitted on : Thursday, January 12, 2017 - 11:34:43 AM
Last modification on : Thursday, February 3, 2022 - 10:04:02 AM
Long-term archiving on: : Friday, April 14, 2017 - 3:16:37 PM


Files produced by the author(s)


Distributed under a Creative Commons Attribution 4.0 International License



Karine Altisen, Pierre Corbineau, Stéphane Devismes. A Framework for Certified Self-Stabilization. 36th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2016, Heraklion, Greece. pp.36-51, ⟨10.1007/978-3-319-39570-8_3⟩. ⟨hal-01432926⟩



Record views


Files downloads