Formal Techniques for Distributed Objects, Components, and Systems 39th IFIP WG 6.1 International Conference, FORTE 2019 Held as Part of the 14th International Federated Conference on Distributed Computing Techniques, DisCoTec 2019 Kongens Lyngby, Denmark, June 17–21, 2019
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.
https://hal.inria.fr/hal-02313746
Contributor : Hal Ifip <>
Submitted on : Friday, October 11, 2019 - 2:55:42 PM Last modification on : Friday, November 20, 2020 - 1:08:01 PM
File
Restricted access
To satisfy the distribution rights of the publisher, the document is embargoed
until : 2022-01-01
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⟩