Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, Epiciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
Skip to Main content Skip to Navigation
Conference papers

Specification-Based Synthesis of Distributed Self-Stabilizing Protocols

Abstract : In this paper, we introduce an SMT-based method that automatically synthesizes a distributed self-stabilizing protocol from a given high-level specification and the network topology. Unlike existing approaches, where synthesis algorithms require the explicit description of the set of legitimate states, our technique only needs the temporal behavior of the protocol. We also extend our approach to synthesize ideal-stabilizing protocols, where every state is legitimate. Our proposed methods are implemented and we report successful synthesis of Dijkstra’s token ring and a self-stabilizing version of Raymond’s mutual exclusion algorithm, as well as ideal-stabilizing leader election and local mutual exclusion.
Complete list of metadata

Cited literature [15 references]  Display  Hide  Download
Contributor : Hal Ifip Connect in order to contact the contributor
Submitted on : Thursday, January 12, 2017 - 11:35:11 AM
Last modification on : Sunday, June 26, 2022 - 9:48:15 AM
Long-term archiving on: : Friday, April 14, 2017 - 5:09:19 PM


Files produced by the author(s)


Distributed under a Creative Commons Attribution 4.0 International License



Fathiyeh Faghih, Borzoo Bonakdarpour, Sébastien Tixeuil, Sandeep Kulkarni. Specification-Based Synthesis of Distributed Self-Stabilizing Protocols. 36th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2016, Heraklion, Greece. pp.124-141, ⟨10.1007/978-3-319-39570-8_9⟩. ⟨hal-01432932⟩



Record views


Files downloads