Faghih, Fathiyeh and Bonakdarpour, Borzoo and Tixeuil, Sebastien and Kulkarni, Sandeep - Automated Synthesis of Distributed Self-Stabilizing Protocols

lmcs:4241 - Logical Methods in Computer Science, January 30, 2018, Volume 14, Issue 1
Automated Synthesis of Distributed Self-Stabilizing Protocols

Authors: Faghih, Fathiyeh and Bonakdarpour, Borzoo and Tixeuil, Sebastien and Kulkarni, Sandeep

In this paper, we introduce an SMT-based method that automatically synthesizes a distributed self-stabilizing protocol from a given high-level specification and 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 extend our approach to synthesize ideal-stabilizing protocols, where every state is legitimate. We also extend our technique to synthesize monotonic-stabilizing protocols, where during recovery, each process can execute an most once one action. Our proposed methods are fully implemented and we report successful synthesis of well-known protocols such as Dijkstra's token ring, a self-stabilizing version of Raymond's mutual exclusion algorithm, ideal-stabilizing leader election and local mutual exclusion, as well as monotonic-stabilizing maximal independent set and distributed Grundy coloring.


Source : oai:arXiv.org:1509.05664
DOI : 10.23638/LMCS-14(1:12)2018
Volume: Volume 14, Issue 1
Published on: January 30, 2018
Submitted on: December 1, 2016
Keywords: Computer Science - Software Engineering,Computer Science - Distributed, Parallel, and Cluster Computing


Share

Consultation statistics

This page has been seen 140 times.
This article's PDF has been downloaded 70 times.