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

https://hal.inria.fr/hal-01432926
Contributor : Hal Ifip <>
Submitted on : Thursday, January 12, 2017 - 11:34:43 AM
Last modification on : Tuesday, May 11, 2021 - 11:36:25 AM
Long-term archiving on: : Friday, April 14, 2017 - 3:16:37 PM

File

426757_1_En_3_Chapter.pdf
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

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⟩

Share

Metrics

Record views

196

Files downloads

446