Advertisement

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

  • Fathiyeh Faghih
  • Borzoo Bonakdarpour
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, 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.

References

  1. 1.
  2. 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_16CrossRefGoogle Scholar
  3. 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. 4.
    Dijkstra, E.W.: Self-stabilizing systems in spite of distributed control. Commun. ACM 17(11), 643–644 (1974)CrossRefGoogle Scholar
  5. 5.
    Dijkstra, E.W.: A belated proof of self-stabilization. Distrib. Comput. 1(1), 5–6 (1986)CrossRefGoogle Scholar
  6. 6.
    Dolev, S., Schiller, E.: Self-stabilizing group communication in directed networks. Acta Informatica 40(9), 609–636 (2004)MathSciNetCrossRefGoogle Scholar
  7. 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. 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)CrossRefGoogle Scholar
  9. 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_25CrossRefGoogle Scholar
  10. 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_12CrossRefGoogle Scholar
  11. 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. 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_9CrossRefGoogle Scholar
  13. 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. 14.
    Finkbeiner, B., Schewe, S.: Bounded synthesis. Int. J. Softw. Tools Technol. Transf. (STTT) 15(5–6), 519–539 (2013)CrossRefGoogle Scholar
  15. 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_8CrossRefGoogle Scholar
  16. 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_22CrossRefGoogle Scholar
  17. 17.
    Hsu, S.-C., Huang, S.-T.: A self-stabilizing algorithm for maximal matching. Inf. Process. Lett. 43(2), 77–81 (1992)MathSciNetCrossRefGoogle Scholar
  18. 18.
    Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge (2012)Google Scholar
  19. 19.
    Jacobs, S., Bloem, R.: Parameterized synthesis. Logical Methods Comput. Sci. (LMCS) 10(1), 1–29 (2014)MathSciNetzbMATHGoogle Scholar
  20. 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_2CrossRefzbMATHGoogle Scholar
  21. 21.
    Manne, F., Mjelde, M., Pilard, L., Tixeuil, S.: A new self-stabilizing maximal matching algorithm. Theoret. Comput. Sci. 410(14), 1336–1345 (2009)MathSciNetCrossRefGoogle Scholar
  22. 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_6CrossRefGoogle Scholar
  23. 23.
    Pnueli, A.: The temporal logic of programs. In: Symposium on Foundations of Computer Science (FOCS), pp. 46–57 (1977)Google Scholar
  24. 24.
    Raymond, K.: A tree-based algorithm for distributed mutual exclusion. ACM Trans. Comput. Syst. 7, 61–77 (1989)CrossRefGoogle Scholar
  25. 25.
    Tel, G.: Maximal matching stabilizes in quadratic time. Inf. Process. Lett. 49(6), 271–272 (1994)CrossRefGoogle Scholar
  26. 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_34CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  1. 1.Department of Electrical and Computer EngineeringUniversity of TehranTehranIran
  2. 2.Department of Computer ScienceIowa State UniversityAmesUSA

Personalised recommendations