A Framework for Certified Self-Stabilization
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...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2017-11-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/2183/pdf |
| _version_ | 1797268611001221120 |
|---|---|
| author | Karine Altisen Pierre Corbineau Stephane Devismes |
| author_facet | Karine Altisen Pierre Corbineau Stephane Devismes |
| author_sort | Karine Altisen |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-25T01:35:13Z |
| format | Article |
| id | doaj.art-202207486d5b4bc7b864cdab01ff7670 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:35:13Z |
| publishDate | 2017-11-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-202207486d5b4bc7b864cdab01ff76702024-03-08T09:52:12ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742017-11-01Volume 13, Issue 410.23638/LMCS-13(4:14)20172183A Framework for Certified Self-StabilizationKarine AltisenPierre CorbineauStephane Devismeshttps://orcid.org/0000-0002-8032-9732We 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.https://lmcs.episciences.org/2183/pdfcomputer science - distributed, parallel, and cluster computingcomputer science - logic in computer science |
| spellingShingle | Karine Altisen Pierre Corbineau Stephane Devismes A Framework for Certified Self-Stabilization Logical Methods in Computer Science computer science - distributed, parallel, and cluster computing computer science - logic in computer science |
| title | A Framework for Certified Self-Stabilization |
| title_full | A Framework for Certified Self-Stabilization |
| title_fullStr | A Framework for Certified Self-Stabilization |
| title_full_unstemmed | A Framework for Certified Self-Stabilization |
| title_short | A Framework for Certified Self-Stabilization |
| title_sort | framework for certified self stabilization |
| topic | computer science - distributed, parallel, and cluster computing computer science - logic in computer science |
| url | https://lmcs.episciences.org/2183/pdf |
| work_keys_str_mv | AT karinealtisen aframeworkforcertifiedselfstabilization AT pierrecorbineau aframeworkforcertifiedselfstabilization AT stephanedevismes aframeworkforcertifiedselfstabilization AT karinealtisen frameworkforcertifiedselfstabilization AT pierrecorbineau frameworkforcertifiedselfstabilization AT stephanedevismes frameworkforcertifiedselfstabilization |