Advertisement

Declarative Parameterized Verification of Topology-Sensitive Distributed Protocols

  • Sylvain Conchon
  • Giorgio DelzannoEmail author
  • Angelo FerrandoEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11028)

Abstract

We show that Cubicle [9], an SMT-based infinite-state model checker, can be applied as a verification engine for GLog, a logic-based specification language for topology-sensitive distributed protocols with asynchronous communication. Existential coverability queries in GLog can be translated into verification judgements in Cubicle by encoding relational updates rules as unbounded array transitions. We apply the resulting framework to automatically verify a distributed version of the Dining Philosopher mutual exclusion protocol formulated for an arbitrary number of nodes and communication buffers.

Supplementary material

References

  1. 1.
    Abdulla, P.A., Delzanno, G.: Parameterized verification. STTT 18(5), 469–473 (2016)CrossRefGoogle Scholar
  2. 2.
    Abdulla, P.A., Delzanno, G., Ben Henda, N., Rezine, A.: Monotonic abstraction: on efficient verification of parameterized systems. Int. J. Found. Comput. Sci. 20(5), 779–801 (2009)MathSciNetCrossRefGoogle Scholar
  3. 3.
    Alberti, F., Ghilardi, S., Sharygina, N.: A framework for the verification of parameterized infinite-state systems. Fundam. Inform. 150(1), 1–24 (2017)MathSciNetCrossRefGoogle Scholar
  4. 4.
    Ancona, D., Ferrando, A., Mascardi, V.: Parametric runtime verification of multiagent systems. In: Proceedings of the 16th Conference on Autonomous Agents and MultiAgent Systems, AAMAS 2017, São Paulo, Brazil, 8–12 May 2017, pp. 1457–1459 (2017)Google Scholar
  5. 5.
    Bertrand, N., Delzanno, G., König, B., Sangnier, A., Stückrath, J.: On the decidability status of reachability and coverability in graph transformation systems. In: RTA 2012, Volume 15 of LIPIcs, pp. 101–116. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2012)Google Scholar
  6. 6.
    Bertrand, N., Fournier, P., Sangnier, A.: Distributed local strategies in broadcast networks. In: 26th International Conference on Concurrency Theory, CONCUR 2015, Madrid, Spain, 1–4 September 2015, pp. 44–57 (2015)Google Scholar
  7. 7.
    Bloem, R., et al.: Decidability of Parameterized Verification. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers, San Rafael (2015)Google Scholar
  8. 8.
    Bloem, R., et al.: Decidability in parameterized verification. SIGACT News 47(2), 53–64 (2016)MathSciNetCrossRefGoogle Scholar
  9. 9.
    Conchon, S., Goel, A., Krstić, S., Mebsout, A., Zaïdi, F.: Cubicle: a parallel SMT-based model checker for parameterized systems. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 718–724. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-31424-7_55CrossRefGoogle Scholar
  10. 10.
    Conchon, S., Goel, A., Krstic, S., Mebsout, A., Zaïdi, F.: Invariants for finite instances and beyond. In: Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, 20–23 October 2013, pp. 61–68 (2013)Google Scholar
  11. 11.
    Delzanno, G.: Constraint-based verification of parameterized cache coherence protocols. Form. Methods Syst. Des. 23(3), 257–301 (2003)CrossRefGoogle Scholar
  12. 12.
    Delzanno, G.: A logic-based approach to verify distributed protocols. In: Proceedings of the 31st Italian Conference on Computational Logic, Milano, Italy, 20–22 June 2016, pp. 86–101 (2016)Google Scholar
  13. 13.
    Delzanno, G.: A unified view of parameterized verification of abstract models of broadcast communication. STTT 18(5), 475–493 (2016)CrossRefGoogle Scholar
  14. 14.
    Delzanno, G., Sangnier, A., Zavattaro, G.: Parameterized verification of Ad Hoc networks. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 313–327. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-15375-4_22CrossRefGoogle Scholar
  15. 15.
    Delzanno, G., Sangnier, A., Zavattaro, G.: On the power of cliques in the parameterized verification of Ad Hoc networks. In: Hofmann, M. (ed.) FoSSaCS 2011. LNCS, vol. 6604, pp. 441–455. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-19805-2_30CrossRefzbMATHGoogle Scholar
  16. 16.
    Delzanno, G., Sangnier, A., Zavattaro, G.: Verification of Ad Hoc networks with node and communication failures. In: Giese, H., Rosu, G. (eds.) FMOODS/FORTE -2012. LNCS, vol. 7273, pp. 235–250. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-30793-5_15CrossRefGoogle Scholar
  17. 17.
    Delzanno, G., Stückrath, J.: Parameterized verification of graph transformation systems with whole neighbourhood operations. In: Ouaknine, J., Potapov, I., Worrell, J. (eds.) RP 2014. LNCS, vol. 8762, pp. 72–84. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-11439-2_6CrossRefGoogle Scholar
  18. 18.
    Mebsout, A.: Inférence d’invariants pour le model checking de systèmes paramétrés (Invariants inference for model checking of parameterized systems). PhD thesis, University of Paris-Sud, Orsay, France (2014)Google Scholar
  19. 19.
    Namjoshi, K.S., Trefler, R.J.: Uncovering symmetries in irregular process networks. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 496–514. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-35873-9_29CrossRefGoogle Scholar
  20. 20.
    Namjoshi, K.S., Trefler, R.J.: Analysis of dynamic process networks. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 164–178. Springer, Heidelberg (2015).  https://doi.org/10.1007/978-3-662-46681-0_11CrossRefGoogle Scholar
  21. 21.
  22. 22.
  23. 23.

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.LRIUniversité Paris-SudOrsayFrance
  2. 2.DIBRISUniversity of GenovaGenoaItaly

Personalised recommendations