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.
This work was partially supported by the NSF grant CCF-1116546.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
Abdulla, P.A., Jonsson, B.: Model checking of systems with many identical timed processes. Theor. Comput. Sci. 290(1), 241–264 (2003)
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)
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)
Abujarad, F., Kulkarni, S.S.: Automated constraint-based addition of nonmasking and stabilizing fault-tolerance. Theor. Comput. Sci. 412(33), 4228–4246 (2011)
Arora, A., Gouda, M.G.: Closure and convergence: a foundation of fault-tolerant computing. IEEE Trans. Softw. Eng. 19(11), 1015–1027 (1993)
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)
Bertrand, N., Fournier, P.: Parameterized verification of many identical probabilistic timed processes. In: LIPIcs-Leibniz International Proceedings in Informatics, vol. 24 (2013)
Bonakdarpour, B., Kulkarni, S.S.: Towards reusing formal proofs for verification of fault-tolerance. In Workshop in Automated Formal Methods (2006)
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)
Dijkstra, E.W.: Self-stabilizing systems in spite of distributed control. Commun. ACM 17(11), 643–644 (1974)
Dolev, S., Haviv, Y.A.: Self-stabilizing microprocessor: analyzing and overcoming soft errors. IEEE Trans. Comput. 55(4), 385–399 (2006)
Dolev, S., Yagel, R.: Self-stabilizing operating systems. In: Proceedings of the twentieth ACM symposium on Operating systems principles, pages 1–2. ACM (2005)
Ebnenasir, A., Farahat, A.: Swarm synthesis of convergence for symmetric protocols. In: European Dependable Computing Conference, pp. 13–24 (2012)
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)
Emerson, E.A., Namjoshi, K.S.: On reasoning about rings. Int. J. Found. Comput. Sci. 14(4), 527–550 (2003)
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)
Fioravanti, F., Pettorossi, A., Proietti, M., Senni, V.: Generalization strategies for the verification of infinite state systems. TPLP 13(2), 175–199 (2013)
Gordon, M.J.C., Melham, T.F.: Introduction to HOL: A Theorem proving Environment for Higher Order Logic. Cambridge University Press, Cambridge (1993)
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)
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)
Ip, C.N., Dill, D.L.: Verifying systems with replicated components in murphi. Form. Methods Syst. Design 14(3), 273–310 (1999)
Jacobs, S., Bloem, R.: Parameterized synthesis. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 362–376. Springer, Heidelberg (2012)
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)
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)
Klinkhamer, A., Ebnenasir, A.: A parallel tool for automated synthesis of self-stabilization. http://asd.cs.mtu.edu/projects/protocon/
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)
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)
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)
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)
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)
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)
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)
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)
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 1998
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
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)
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)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Tahat, A., Ebnenasir, A. (2015). A Hybrid Method for the Verification and Synthesis of Parameterized Self-Stabilizing Protocols. In: Proietti, M., Seki, H. (eds) Logic-Based Program Synthesis and Transformation. LOPSTR 2014. Lecture Notes in Computer Science(), vol 8981. Springer, Cham. https://doi.org/10.1007/978-3-319-17822-6_12
Download citation
DOI: https://doi.org/10.1007/978-3-319-17822-6_12
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-17821-9
Online ISBN: 978-3-319-17822-6
eBook Packages: Computer ScienceComputer Science (R0)