Advertisement

A Hybrid Method for the Verification and Synthesis of Parameterized Self-Stabilizing Protocols

  • Amer Tahat
  • Ali EbnenasirEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8981)

Abstract

This paper presents a hybrid method for verification and synthesis of parameterized self-stabilizing protocols where algorithmic design and mechanical verification techniques/tools are used hand-in-hand. The core idea behind the proposed method includes the automated synthesis of self-stabilizing protocols in a limited scope (i.e., fixed number of processes) and the use of theorem proving methods for the generalization of the solutions produced by the synthesizer. Specifically, we use the Prototype Verification System (PVS) to mechanically verify an algorithm for the synthesis of weakly self-stabilizing protocols. Then, we reuse the proof of correctness of the synthesis algorithm to establish the correctness of the generalized versions of synthesized protocols for an arbitrary number of processes. We demonstrate the proposed approach in the context of an agreement and a coloring protocol on the ring topology.

Keywords

Mechanical verification Program synthesis Self-stabilization Parameterized systems 

References

  1. 1.
    Abdulla, P.A., Jonsson, B.: Model checking of systems with many identical timed processes. Theor. Comput. Sci. 290(1), 241–264 (2003)CrossRefzbMATHMathSciNetGoogle Scholar
  2. 2.
    Abdulla, P.A., Jonsson, B., Nilsson, M., Saksena, M.: A survey of regular model checking. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 35–48. Springer, Heidelberg (2004) CrossRefGoogle Scholar
  3. 3.
    Abujarad, F., Kulkarni, S.S.: Multicore constraint-based automated stabilization. In: Guerraoui, R., Petit, F. (eds.) SSS 2009. LNCS, vol. 5873, pp. 47–61. Springer, Heidelberg (2009) CrossRefGoogle Scholar
  4. 4.
    Abujarad, F., Kulkarni, S.S.: Automated constraint-based addition of nonmasking and stabilizing fault-tolerance. Theor. Comput. Sci. 412(33), 4228–4246 (2011)CrossRefzbMATHMathSciNetGoogle Scholar
  5. 5.
    Arora, A., Gouda, M.G.: Closure and convergence: a foundation of fault-tolerant computing. IEEE Trans. Softw. Eng. 19(11), 1015–1027 (1993)CrossRefGoogle Scholar
  6. 6.
    Attie, P.C., Arora, A., Emerson, E.A.: Synthesis of fault-tolerant concurrent programs. ACM Trans. Program. Lang. Syst (TOPLAS) 26(1), 125–185 (2004)CrossRefGoogle Scholar
  7. 7.
    Bertrand, N., Fournier, P.: Parameterized verification of many identical probabilistic timed processes. In: LIPIcs-Leibniz International Proceedings in Informatics, vol. 24 (2013)Google Scholar
  8. 8.
    Bonakdarpour, B., Kulkarni, S.S.: Towards reusing formal proofs for verification of fault-tolerance. In Workshop in Automated Formal Methods (2006)Google Scholar
  9. 9.
    Bouajjani, A., Jonsson, B., Nilsson, M., Touili, T.: Regular model checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 403–418. Springer, Heidelberg (2000) CrossRefGoogle Scholar
  10. 10.
    Dijkstra, E.W.: Self-stabilizing systems in spite of distributed control. Commun. ACM 17(11), 643–644 (1974)CrossRefzbMATHGoogle Scholar
  11. 11.
    Dolev, S., Haviv, Y.A.: Self-stabilizing microprocessor: analyzing and overcoming soft errors. IEEE Trans. Comput. 55(4), 385–399 (2006)CrossRefGoogle Scholar
  12. 12.
    Dolev, S., Yagel, R.: Self-stabilizing operating systems. In: Proceedings of the twentieth ACM symposium on Operating systems principles, pages 1–2. ACM (2005)Google Scholar
  13. 13.
    Ebnenasir, A., Farahat, A.: Swarm synthesis of convergence for symmetric protocols. In: European Dependable Computing Conference, pp. 13–24 (2012)Google Scholar
  14. 14.
    Ebnenasir, A., Kulkarni, S.S., Arora, A.: FTSyn: a framework for automatic synthesis of fault-tolerance. Int. J. Softw. Tools Technol. Transf. 10(5), 455–471 (2008)CrossRefGoogle Scholar
  15. 15.
    Emerson, E.A., Namjoshi, K.S.: On reasoning about rings. Int. J. Found. Comput. Sci. 14(4), 527–550 (2003)CrossRefzbMATHMathSciNetGoogle Scholar
  16. 16.
    Farahat, A., Ebnenasir, A.: A lightweight method for automated design of convergence in network protocols. ACM Trans. Auton. Adapt. Syst. (TAAS) 7(4), 38:1–38:36 (2012)Google Scholar
  17. 17.
    Fioravanti, F., Pettorossi, A., Proietti, M., Senni, V.: Generalization strategies for the verification of infinite state systems. TPLP 13(2), 175–199 (2013)zbMATHMathSciNetGoogle Scholar
  18. 18.
    Gordon, M.J.C., Melham, T.F.: Introduction to HOL: A Theorem proving Environment for Higher Order Logic. Cambridge University Press, Cambridge (1993) zbMATHGoogle Scholar
  19. 19.
    Gouda, M.G.: The theory of weak stabilization. In: Datta, A.K., Herman, T. (eds.) WSS 2001. LNCS, vol. 2194, p. 114. Springer, Heidelberg (2001) CrossRefGoogle Scholar
  20. 20.
    Grinchtein, O., Leucker, M., Piterman, N.: Inferring network invariants automatically. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 483–497. Springer, Heidelberg (2006) CrossRefGoogle Scholar
  21. 21.
    Ip, C.N., Dill, D.L.: Verifying systems with replicated components in murphi. Form. Methods Syst. Design 14(3), 273–310 (1999)CrossRefGoogle Scholar
  22. 22.
    Jacobs, S., Bloem, R.: Parameterized synthesis. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 362–376. Springer, Heidelberg (2012) CrossRefGoogle Scholar
  23. 23.
    Kesten, Y., Pnueli, A., Shahar, E., Zuck, L.D.: Network invariants in action. In: Brim, L., Jančar, P., Křetínský, M., Kučera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 101–115. Springer, Heidelberg (2002) CrossRefGoogle Scholar
  24. 24.
    Khalimov, A., Jacobs, S., Bloem, R.: PARTY Parameterized Synthesis of Token Rings. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 928–933. Springer, Heidelberg (2013) CrossRefGoogle Scholar
  25. 25.
    Klinkhamer, A., Ebnenasir, A.: A parallel tool for automated synthesis of self-stabilization. http://asd.cs.mtu.edu/projects/protocon/
  26. 26.
    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) CrossRefGoogle Scholar
  27. 27.
    Kulkarni, S.S., Arora, A.: Large automating the addition of fault-tolerance. In: Joseph, M. (ed.) FTRTFT 2000. LNCS, vol. 1926, p. 82. Springer, Heidelberg (2000) CrossRefGoogle Scholar
  28. 28.
    Kulkarni, S.S., Bonakdarpour, B., Ebnenasir, A.: Mechanical verification of automatic synthesis of fault-tolerance. Int. Symp. Log.-based Program Synth. Transform. 3573, 36–52 (2004)MathSciNetGoogle Scholar
  29. 29.
    Kulkarni, S.S., Rushby, J., Shankar, N.: A case-study in component-based mechanical verification of fault-tolerant programs. In: 19th IEEE International Conference on Distributed Computing Systems - Workshop on Self-Stabilizing Systems, pp. 33–40 (1999)Google Scholar
  30. 30.
    Pnueli, A., Xu, J., Zuck, L.D.: Liveness with \({(0,1,\infty )}\)-Counter Abstraction. In: Brinksma, Ed, Larsen, Kim Guldstrand (eds.) CAV 2002. LNCS, vol. 2404, pp. 107–. Springer, Heidelberg (2002)Google Scholar
  31. 31.
    Prasetya, I.S.W.B.: Mechanically verified self-stabilizing hierarchical algorithms. Tools and Algorithms for the Construction and Analysis of Systems (TACAS’97), volume 1217 of Lecture Notes in Computer Science, pages 399–415 (1997)Google Scholar
  32. 32.
    Qadeer, S., Shankar, N.: Verifying a self-stabilizing mutual exclusion algorithm. In: Gries, D., de Roever, W.-P. (eds.) IFIP International Conference on Programming Concepts and Methods (PROCOMET 1998), pp. 424–443. Chapman & Hall, Shelter Island, NY (1998) CrossRefGoogle Scholar
  33. 33.
    Roychoudhury, A., Narayan Kumar, K., Ramakrishnan, C.R., Ramakrishnan, I.V., Smolka, S.A.: Verification of Parameterized Systems Using Logic Program Transformations. In: Graf, S. (ed.) TACAS 2000. LNCS, vol. 1785, p. 172. Springer, Heidelberg (2000) CrossRefGoogle Scholar
  34. 34.
    Shankar, N., Owre, S., Rushby, J.M.: The PVS Proof Checker: A Reference Manual. Computer Science Laboratory, SRI International, Menlo Park, CA, Feb. 1993. A new edition for PVS Version 2 is released in 1998Google Scholar
  35. 35.
    Tahat, A., Ebnenasir, A.: A hybrid method for the verification and synthesis of parameterized self-stabilizing protocols. Technical Report CS-TR-14-02, Michigan Technological University, May 2014. http://www.mtu.edu/cs/research/papers/pdfs/Technical%20Report%2014-02.pdf
  36. 36.
    Tsuchiya, T., Nagano, S., Paidi, R.B., Kikuno, T.: Symbolic model checking for self-stabilizing algorithms. IEEE Trans. Parallel Distrib. Syst. 12(1), 81–95 (2001)CrossRefGoogle Scholar
  37. 37.
    Wolper, P., Lovinfosse, V.: Verifying properties of large sets of processes with network invariants. In: International Workshop on Automatic Verification Methods for Finite State Systems, pp. 68–80 (1989)Google Scholar

Copyright information

© Springer International Publishing Switzerland 2015

Authors and Affiliations

  1. 1.Department of Computer ScienceMichigan Technological UniversityHoughtonUSA

Personalised recommendations