Fathiyeh Faghih
Abstract
A self-stabilizing system is one that guarantees reaching a set of legitimate states from any arbitrary initial state. Designing distributed self-stabilizing protocols is often a complex task and developing their proof of correctness is known to be significantly more tedious. In this article, we propose an SMT-based method that automatically synthesizes a self-stabilizing protocol, given the network topology of distributed processes and description of the set of legitimate states. Our method can synthesize synchronous, asynchronous, symmetric, and asymmetric protocols for two types of stabilization, namely weak and strong. We also report on successful automated synthesis of a set of well-known distributed stabilizing protocols such as Dijkstra’s token ring, distributed maximal matching, graph coloring, and mutual exclusion in anonymous networks.
- F. Abujarad and S. S. Kulkarni. 2011. Automated constraint-based addition of nonmasking and stabilizing fault-tolerance. Theoretical Computer Science 412, 33, 4228--4246.Google Scholar
Cross Ref
- A. Arora, M. G. Gouda, and G. Varghese. 1996. Constraint satisfaction as a basis for designing nonmasking fault-tolerance. Journal of High Speed Networks 5, 3, 293--306. Google ScholarDigital Library
- B. Bonakdarpour, S. S. Kulkarni, and F. Abujarad. 2012. Symbolic synthesis of masking fault-tolerant programs. Journal on Distributed Computing 25, 1, 83--108.Google ScholarCross Ref
- E. M. Clarke, A. Biere, R. Raimi, and Y. Zhu. 2001. Bounded model checking using satisfiability solving. Formal Methods in System Design 19, 1, 7--34. Google ScholarDigital Library
- W. Damm and B. Finkbeiner. 2014. Automatic compositional synthesis of distributed systems. In Proceedings of the 19th International Symposium on Formal Methods (FM). 179--193.Google Scholar
- S. Devismes, S. Tixeuil, and M. Yamashita. 2008. Weak vs. self vs. probabilistic stabilization. In Proceedings of the 28th IEEE International Conference on Distributed Computing Systems (ICDCS). 681--688. Google ScholarDigital Library
- E. W. Dijkstra. 1974. Self-stabilizing systems in spite of distributed control. Communications of the ACM 17, 11, 643--644. Google ScholarDigital Library
- E. W. Dijkstra. 1986. A belated proof of self-stabilization. Distributed Computing 1, 1, 5--6. Google ScholarDigital Library
- R. Dimitrova and B. Finkbeiner. 2009. Synthesis of fault-tolerant distributed systems. In Proceedings of the 7th International Symposium on Automated Technology for Verification and Analysis (ATVA). 321--336. Google ScholarDigital Library
- S. Dolev and E. Schiller. 2004. Self-stabilizing group communication in directed networks. Acta Informatica 40, 9, 609--636. Google ScholarDigital Library
- A. Ebnenasir and A. Farahat. 2011. A lightweight method for automated design of convergence. In Proceedings of the 25th IEEE International Parallel and Distributed Processing Symposium (IPDPS). 219--230. Google ScholarDigital Library
- E. A. Emerson. 1990. Temporal and Modal Logics. In Handbook of Theoretical Computer Science. Jan van Leeuwen (eds), Vol. B. Elsevier Science Publishers B. V., Amsterdam, The Netherlands. Google ScholarDigital Library
- B. Finkbeiner and E.-R. Olderog. 2014. Petri games: Synthesis of distributed systems with causal memory. In Proceedings of the 5th International Symposium on Games, Automata, Logics and Formal Verification (GandALF). 217--230.Google ScholarCross Ref
- B. Finkbeiner and S. Schewe. 2013. Bounded synthesis. International Journal on Software Tools for Technology Transfer (STTT) 15, 5--6, 519--539.Google ScholarDigital Library
- A. Gascón and A. Tiwari. 2014. Synthesis of a simple self-stabilizing system. In Proceedings of the 3rd Workshop on Synthesis (SYNT). 5--16.Google Scholar
- M. G. Gouda. 2001. The theory of weak stabilization. In International Workshop on Self-Stabilizing Systems. 114--123. Google ScholarDigital Library
- M. G. Gouda and H. B. Acharya. 2009. Nash equilibria in stabilizing systems. In Proceedings of the 11th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS). 311--324. Google ScholarDigital Library
- T. Herman. 1990. Probabilistic self-stabilization. Information Processing Letters 35, 2, 63--67. Google ScholarDigital Library
- S.-C. Hsu and S.-T. Huang. 1992. A self-stabilizing algorithm for maximal matching. Information Processing Letters 43, 2, 77--81. Google ScholarDigital Library
- D. Jackson. 2012. Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge, MA. Google ScholarDigital Library
- S. Jacobs and R. Bloem. 2014. Parameterized synthesis. Logical Methods in Computer Science 10, 1.Google ScholarCross Ref
- A. Klinkhamer and A. Ebnenasir. 2013. On the complexity of adding convergence. In Proceedings of the International Conference on Fundamentals of Software Engineering. 17--33.Google Scholar
- A. Klinkhamer and A. Ebnenasir. 2014. Synthesizing self-stabilization through superposition and backtracking. In Proceedings of the 16th International Symposium on Stabilization, Safety, and Security of Distributed Systems. 252--267.Google Scholar
- O. Kupferman and M. Y. Vardi. 2005. Safraless decision procedures. In Proceedings of 46th Annual IEEE Symposium on Foundations of Computer Science (FOCS). 531--542. Google ScholarDigital Library
- Y. Lin, B. Bonakdarpour, and S. S. Kulkarni. 2013. Automated addition of fault-tolerance under synchronous semantics. In Proceedings of the 15th International Symposium on Stabilization, Safety, and Security of Distributed Systems. 266--280. Google ScholarDigital Library
- N. Lynch. 1996. Distributed Algorithms. Morgan Kaufmann Publishers, San Mateo, CA. Google ScholarDigital Library
- F. Manne, M. Mjelde, L. Pilard, and S. Tixeuil. 2009. A new self-stabilizing maximal matching algorithm. Theoretical Computer Science 410, 14, 1336--1345. Google ScholarDigital Library
- F. Ooshita and S. Tixeuil. 2012. On the self-stabilization of mobile oblivious robots in uniform rings. In International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS). 49--63. Google ScholarDigital Library
- K. Raymond. 1989. A tree-based algorithm for distributed mutual exclusion. ACM Transactions on Computer Systems 7, 61--77. Google ScholarDigital Library
- G. Tel. 1994. Maximal matching stabilizes in quadratic time. Information Processing Letters 49, 6, 271--272. Google ScholarDigital Library
Index Terms
- SMT-Based Synthesis of Distributed Self-Stabilizing Systems
Recommendations
Fault-containing self-stabilizing distributed protocols
Self-stabilization is an elegant approach for designing a class of fault-tolerant distributed protocols. A self-stabilizing protocol is guaranteed to eventually converge to a legitimate state after a transient fault. However, even a minor transient ...
Automated Synthesis of Multitolerance
DSN '04: Proceedings of the 2004 International Conference on Dependable Systems and NetworksWe concentrate on automated synthesis of multitolerant programs,i.e., programs that tolerate multiple classes of faultsand provide a (possibly) different level of fault-tolerance toeach class. We consider three levels of fault-tolerance: (1)failsafe, ...
A Byzantine-fault tolerant self-stabilizing protocol for distributed clock synchronization systems
SSS'06: Proceedings of the 8th international conference on Stabilization, safety, and security of distributed systemsEmbedded distributed systems have become an integral part of safety-critical computing applications, necessitating system designs that incorporate fault tolerant clock synchronization in order to achieve ultra-reliable assurance levels. Many efficient ...
Comments