Skip to Main content Skip to Navigation
Conference papers

Squeezing Streams and Composition of Self-stabilizing Algorithms

Abstract : Composition is a fundamental tool when dealing with complex systems. We study the hierarchical collateral composition which is used to combine self-stabilizing distributed algorithms. The PADEC library is a framework developed with the Coq proof assistant and dedicated to the certification of self-stabilizing algorithms. We enrich PADEC with the composition operator and a sufficient condition to show its correctness. The formal proof of the condition leads us to develop new tools and methods on potentially infinite streams, these latter ones being used to model the algorithms’ executions. The cornerstone has been the definition of the function which removes duplicates from streams.
Complete list of metadata

Cited literature [35 references]  Display  Hide  Download

https://hal.inria.fr/hal-02313746
Contributor : Hal Ifip Connect in order to contact the contributor
Submitted on : Friday, October 11, 2019 - 2:55:42 PM
Last modification on : Wednesday, November 3, 2021 - 4:31:26 AM

File

478668_1_En_2_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. Squeezing Streams and Composition of Self-stabilizing Algorithms. 39th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2019, Copenhagen, Denmark. pp.21-38, ⟨10.1007/978-3-030-21759-4_2⟩. ⟨hal-02313746⟩

Share

Metrics

Les métriques sont temporairement indisponibles