Declarative Parameterized Verification of Distributed Protocols via the Cubicle Model Checker

• Autorzy: Conchon Sylvain , Delzanno Giorgio , Ferrando Angelo

Identyfikatory

DOI

10.3233/FI-2021-2010

• Języki publikacji: EN

Abstrakty

EN

We show that Cubicle, an SMT-based infinite-state model checker, can be applied as a verification engine for GLog, a logic-based language based on relational updates rules that has been applied to specify topology-sensitive distributed protocols with asynchronous communication. In this setting, the absence of protocol anomalies can be reduced to a coverability problem in which the initial set of configurations is not fixed a priori (Existential Coverability Problem). Existential Coverability in GLog can naturally be expressed into Parameterized Verification judgements in Cubicle. The encoding is based on a translation of relational update rules into transition rules that modify cells of unbounded arrays. To show the effectiveness of the approach, we discuss several verification problems for distributed protocols and distributed objects, a challenging task for traditional verification tools. The experimental results show the flexibility and robustness of Cubicle for the considered class of protocol examples.

Słowa kluczowe

EN

tissue arrays; translating; interpreting

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2021
• Tom: Vol. 178, nr 4
• Strony: 347--378
• Opis fizyczny: Bibliogr. 32 poz., tab.

Twórcy

autor

Conchon Sylvain

• LRI, Université Paris-Saclay, France

autor

Delzanno Giorgio

• DIBRIS, University of Genova, Italy

autor

Ferrando Angelo

• The University of Manchester, United Kingdom

Bibliografia

• [1] Bloem R, Jacobs S, Khalimov A, Konnov I, Rubin S, Veith H, Widder J. Decidability of Parameterized Verification. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers, 2015. doi:10.2200/S00658ED1V01Y201508DCT013.
• [2] Bloem R, Jacobs S, Khalimov A, Konnov I, Rubin S, Veith H, Widder J. Decidability in Parameterized Verification. SIGACT News, 2016. 47(2):53-64. doi:10.2200/S00658ED1V01Y201508DCT013.
• [3] 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’12, volume 15 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2012 pp. 101-116. doi:10.4230/LIPIcs.RTA.2012.101.
• [4] Bertrand N, Fournier P, Sangnier A. Distributed Local Strategies in Broadcast Networks. In: 26th International Conference on Concurrency Theory, CONCUR 2015, Madrid, Spain, September 1.4, 2015. 2015 pp. 44-57. doi:10.4230/LIPIcs.CONCUR.2015.44.
• [5] Delzanno G, Sangnier A, Zavattaro G. Parameterized Verification of Ad Hoc Networks. In: CONCUR 2010 - Concurrency Theory, 21th International Conference, CONCUR 2010, Paris, France, August 31- September 3, 2010. Proceedings. 2010 pp. 313-327. doi:10.1007/978-3-642-15375-4\_22.
• [6] Delzanno G, Sangnier A, Zavattaro G. On the Power of Cliques in the Parameterized Verification of Ad Hoc Networks. In: Foundations of Software Science and Computational Structures - 14th International Conference, FOSSACS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26-April 3, 2011. Proceedings. 2011 pp. 441-455. doi:10.1007/978-3-642-19805-2\_30.
• [7] Delzanno G, Sangnier A, Zavattaro G. Verification of Ad Hoc Networks with Node and Communication Failures. In: FORTE/FMOODS’12, volume 7273 of LNCS. Springer, 2012 pp. 235-250. doi:10.1007/978-3-642-30793-5_15.
• [8] Abdulla PA, Delzanno G. Parameterized verification. STTT, 2016. 18(5):469-473. doi:10.1007/s10009-016-0424-3.
• [9] Delzanno G. A unified view of parameterized verification of abstract models of broadcast communication. STTT, 2016. 18(5):475-493. doi:10.1007/s10009-016-0412-7.
• [10] Delzanno G. Constraint-Based Verification of Parameterized Cache Coherence Protocols. Formal Methods in System Design, 2003. 23(3):257-301. doi:10.1023/A:1026276129010.
• [11] Larsen KG, Pettersson P, Yi W. UPPAAL in a Nutshell. Int. Journal on Software Tools for Technology Transfer, 1997. 1(1-2):134-152. ISSN:1433-2779.
• [12] Behrmann G, David A, Larsen KG, OMöller, Pettersson P, Yi W. UPPAAL - Present and Future. In: Proc. of 40th IEEE Conference on Decision and Control. 2001. doi:10.1109/CDC.2001.980713.
• [13] Holzmann GJ. The SPIN Model Checker - primer and reference manual. Addison-Wesley, 2004. ISBN:978-0-321-22862-8.
• [14] Rozenberg G (ed.). Handbook of Graph Grammars and Computing by Graph Transformations, Volume 1: Foundations. World Scientific, 1997. ISBN:9810228848.
• [15] Ghamarian AH, de Mol M, Rensink A, Zambon E, Zimakova M. Modelling and analysis using GROOVE. STTT, 2012. 14(1):15-40. doi:10.1007/s10009-011-0186-x.
• [16] Delzanno G. A Logic-based Approach to Verify Distributed Protocols. In: Proceedings of the 31st Italian Conference on Computational Logic, Milano, Italy, June 20-22, 2016 pp. 86-101. ID:15697605.
• [17] Delzanno G. Logic-based Verification of the Distributed Dining Philosophers Protocol. Fundam. Inform., 2018. 161(1-2):113-133. doi:10.3233/FI-2018-1697.
• [18] http://wwwdisiunigeit/person/DelzannoG/MSR/.
• [19] Abdulla PA, Delzanno G, Henda NB, Rezine A. Monotonic Abstraction: on Efficient Verification of Parameterized Systems. International Journal of Foundations of Computer Science, 2009. 20(5):779-801. doi:10.1142/S0129054109006887.
• [20] Conchon S, Goel A, Krstic S, Mebsout A, Zaïdi F. Cubicle: A Parallel SMT-Based Model Checker for Parameterized Systems - Tool Paper. In: Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings. 2012 pp. 718-724. doi:10.1007/978-3-642-31424-7_55.
• [21] Mebsout A. Inférence d’invariants pour le model checking de systèmes paramétrés. (Invariants inference for model checking of parameterized systems). Ph.D. thesis, University of Paris-Sud, Orsay, France, 2014.
• [22] Alberti F, Ghilardi S, Sharygina N. A Framework for the Verification of Parameterized Infinite-state Systems. Fundam. Inform., 2017. 150(1):1-24. doi:10.3233/FI-2017-1458.
• [23] Conchon S, Delzanno G, Ferrando A. Declarative Parameterized Verification of Topology-Sensitive Distributed Protocols. In: Networked Systems - 6th International Conference, NETYS 2018, Essaouira, Morocco, May 9-11, 2018, Revised Selected Papers. 2018 pp. 209-224. doi:10.1007/978-3-030-05529-5_14.
• [24] Delzanno G, Stückrath J. Parameterized Verification of Graph Transformation Systems with Whole Neighbourhood Operations. In: Reachability Problems - 8th International Workshop, RP 2014, Oxford, UK, September 22-24, 2014. Proceedings. 2014 pp. 72-84. doi:10.1007/978-3-319-11439-2_6.
• [25] Namjoshi KS, Trefler RJ. Analysis of Dynamic Process Networks. In: Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings. 2015 pp. 164-178. doi:10.1007/978-3-662-46681-0_11.
• [26] http://alt-ergolrifr.
• [27] http://functorylrifr/.
• [28] Dill DL. The Murphi Verification System. In: Computer Aided Verification, 8th International Conference, CAV ’96, New Brunswick, NJ, USA, July 31 - August 3, 1996, Proceedings, volume 1102 of Lecture Notes in Computer Science. 1996 pp. 390-393.
• [29] Bryant RE, Lahiri SK, Seshia SA. Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions. In: Computer Aided Verification, 14th International Conference, CAV 2002,Copenhagen, Denmark, July 27-31, 2002, Proceedings, volume 2404 of Lecture Notes in Computer Science. 2002 pp. 78-92. doi:10.1007/3-540-45657-0_7.
• [30] 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, October 20-23, 2013. 2013 pp. 61-68. doi:10.1109/FMCAD.2013.6679392.
• [31] Namjoshi KS, Trefler RJ. Uncovering Symmetries in Irregular Process Networks. In: VMCAI. 2013 pp. 496-514. doi:10.1007/978-3-642-35873-9_29.
• [32] Ancona D, 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, May 8-12, 2017. 2017 pp. 1457-1459.

Uwagi

Opracowanie rekordu ze środków MNiSW, umowa Nr 461252 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2021).