Skip to main content
SpringerLink
Log in

ASSESS: A Tool for Automated Synthesis of Distributed Self-stabilizing Algorithms

  • Conference paper
  • First Online:
Stabilization, Safety, and Security of Distributed Systems (SSS 2017)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10616))

Abstract

A distributed self-stabilizing system is one that always recovers to its legitimate behavior with no external intervention, even if it is initialized in an arbitrary state. It is well known that designing and reasoning about the correctness of such protocols are highly tedious and complex tasks. We present Assess (Automated Synthesizer for SElf-Stabilizing Systems), a tool that automatically synthesizes distributed self-stabilizing algorithms from their high-level specification. Assess takes as input (1) the network topology of the distributed system, (2) the legitimate behavior of the system (either explicitly as a state predicate, or implicitly as a set of ltl formulas), and (3) a set of high-level requirements such as the timing model (asynchronous or synchronous) and stabilization type (weak, strong, and monotonic). The tool utilizes powerful SMT-solving techniques and returns a self-stabilizing protocol as a set of guarded commands that realize the input specification. Since the output is correct by construction, it will not need any proof correctness. We expect the designers and researchers in the area of self-stabilization to significantly benefit from the tool.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Notes

  1. 1.

    The tool can be accessed at http://www.cas.mcmaster.ca/borzoo/assess.

References

  1. Z3: An efficient theorem prover. http://research.microsoft.com/en-us/um/redmond/projects/z3/

  2. Bonakdarpour, B., Kulkarni, S.S.: SYCRAFT: a tool for synthesizing distributed fault-tolerant programs. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 167–171. Springer, Heidelberg (2008). doi:10.1007/978-3-540-85361-9_16

    Chapter  Google Scholar 

  3. Devismes, S., Tixeuil, S., Yamashita, M.: Weak vs. self vs. probabilistic stabilization. In: International Conference on Distributed Computing Systems (ICDCS), pp. 681–688 (2008)

    Google Scholar 

  4. Dijkstra, E.W.: Self-stabilizing systems in spite of distributed control. Commun. ACM 17(11), 643–644 (1974)

    Article  Google Scholar 

  5. Dijkstra, E.W.: A belated proof of self-stabilization. Distrib. Comput. 1(1), 5–6 (1986)

    Article  Google Scholar 

  6. Dolev, S., Schiller, E.: Self-stabilizing group communication in directed networks. Acta Informatica 40(9), 609–636 (2004)

    Article  MathSciNet  Google Scholar 

  7. Ebnenasir, A., Farahat, A.: A lightweight method for automated design of convergence. In: International Parallel and Distributed Processing Symposium (IPDPS), pp. 219–230 (2011)

    Google Scholar 

  8. Ebnenasir, A., Kulkarni, S.S., Arora, A.: FTSyn: a framework for automatic synthesis of fault-tolerance. Int. J. Softw. Tools Technol. Transf. (STTT) 10(5), 455–471 (2008)

    Article  Google Scholar 

  9. Ehlers, R.: Unbeast: symbolic bounded synthesis. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 272–275. Springer, Heidelberg (2011). doi:10.1007/978-3-642-19835-9_25

    Chapter  Google Scholar 

  10. Faghih, F., Bonakdarpour, B.: SMT-based synthesis of distributed self-stabilizing systems. In: Felber, P., Garg, V. (eds.) SSS 2014. LNCS, vol. 8756, pp. 165–179. Springer, Cham (2014). doi:10.1007/978-3-319-11764-5_12

    Chapter  Google Scholar 

  11. Faghih, F., Bonakdarpour, B.: SMT-based synthesis of distributed self-stabilizing systems. ACM Trans. Auton. Adapt. Syst. (TAAS) 10(3), 21 (2015)

    Google Scholar 

  12. Faghih, F., Bonakdarpour, B., Tixeuil, S., Kulkarni, S.: Specification-based synthesis of distributed self-stabilizing protocols. In: Albert, E., Lanese, I. (eds.) FORTE 2016. LNCS, vol. 9688, pp. 124–141. Springer, Cham (2016). doi:10.1007/978-3-319-39570-8_9

    Chapter  Google Scholar 

  13. Farahat, A., Ebnenasir, A.: A lightweight method for automated design of convergence in network protocols. ACM Trans. Auton. Adapt. Syst. (TAAS) 7(4), 38 (2012)

    Google Scholar 

  14. Finkbeiner, B., Schewe, S.: Bounded synthesis. Int. J. Softw. Tools Technol. Transf. (STTT) 15(5–6), 519–539 (2013)

    Article  Google Scholar 

  15. Gouda, M.G.: The theory of weak stabilization. In: Datta, A.K., Herman, T. (eds.) WSS 2001. LNCS, vol. 2194, pp. 114–123. Springer, Heidelberg (2001). doi:10.1007/3-540-45438-1_8

    Chapter  Google Scholar 

  16. Gouda, M.G., Acharya, H.B.: Nash equilibria in stabilizing systems. In: Guerraoui, R., Petit, F. (eds.) SSS 2009. LNCS, vol. 5873, pp. 311–324. Springer, Heidelberg (2009). doi:10.1007/978-3-642-05118-0_22

    Chapter  Google Scholar 

  17. Hsu, S.-C., Huang, S.-T.: A self-stabilizing algorithm for maximal matching. Inf. Process. Lett. 43(2), 77–81 (1992)

    Article  MathSciNet  Google Scholar 

  18. Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge (2012)

    Google Scholar 

  19. Jacobs, S., Bloem, R.: Parameterized synthesis. Logical Methods Comput. Sci. (LMCS) 10(1), 1–29 (2014)

    MathSciNet  MATH  Google Scholar 

  20. Klinkhamer, A., Ebnenasir, A.: On the complexity of adding convergence. In: Arbab, F., Sirjani, M. (eds.) FSEN 2013. LNCS, vol. 8161, pp. 17–33. Springer, Heidelberg (2013). doi:10.1007/978-3-642-40213-5_2

    Chapter  MATH  Google Scholar 

  21. Manne, F., Mjelde, M., Pilard, L., Tixeuil, S.: A new self-stabilizing maximal matching algorithm. Theoret. Comput. Sci. 410(14), 1336–1345 (2009)

    Article  MathSciNet  Google Scholar 

  22. Ooshita, F., Tixeuil, S.: On the self-stabilization of mobile oblivious robots in uniform rings. In: Richa, A.W., Scheideler, C. (eds.) SSS 2012. LNCS, vol. 7596, pp. 49–63. Springer, Heidelberg (2012). doi:10.1007/978-3-642-33536-5_6

    Chapter  Google Scholar 

  23. Pnueli, A.: The temporal logic of programs. In: Symposium on Foundations of Computer Science (FOCS), pp. 46–57 (1977)

    Google Scholar 

  24. Raymond, K.: A tree-based algorithm for distributed mutual exclusion. ACM Trans. Comput. Syst. 7, 61–77 (1989)

    Article  Google Scholar 

  25. Tel, G.: Maximal matching stabilizes in quadratic time. Inf. Process. Lett. 49(6), 271–272 (1994)

    Article  Google Scholar 

  26. Yamauchi, Y., Tixeuil, S.: Monotonic stabilization. In: Lu, C., Masuzawa, T., Mosbah, M. (eds.) OPODIS 2010. LNCS, vol. 6490, pp. 475–490. Springer, Heidelberg (2010). doi:10.1007/978-3-642-17653-1_34

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Electrical and Computer Engineering, University of Tehran, Tehran, Iran

    Fathiyeh Faghih

  2. Department of Computer Science, Iowa State University, Ames, IA, USA

    Borzoo Bonakdarpour

Authors
  1. Fathiyeh Faghih
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Borzoo Bonakdarpour
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to Fathiyeh Faghih or Borzoo Bonakdarpour .

Editor information

Editors and Affiliations

  1. University of Liverpool, Liverpool, United Kingdom

    Paul Spirakis

  2. Chalmers University of Technology, Gothenburg, Sweden

    Philippas Tsigas

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Faghih, F., Bonakdarpour, B. (2017). ASSESS: A Tool for Automated Synthesis of Distributed Self-stabilizing Algorithms. In: Spirakis, P., Tsigas, P. (eds) Stabilization, Safety, and Security of Distributed Systems. SSS 2017. Lecture Notes in Computer Science(), vol 10616. Springer, Cham. https://doi.org/10.1007/978-3-319-69084-1_15

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-69084-1_15

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-69083-4

  • Online ISBN: 978-3-319-69084-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation