A Framework for Certified Self-Stabilization - Formal Techniques for Distributed Objects, Components, and Systems Access content directly
Conference Papers Year : 2016

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.
Fichier principal
Vignette du fichier
426757_1_En_3_Chapter.pdf (311.94 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01432926 , version 1 (12-01-2017)

Licence

Attribution

Identifiers

Cite

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⟩
105 View
62 Download

Altmetric

Share

Gmail Facebook X LinkedIn More