Top

Published in:

2019 | OriginalPaper | Chapter

Declarative Parameterized Verification of Topology-Sensitive Distributed Protocols

Authors : Sylvain Conchon, Giorgio Delzanno, Angelo Ferrando

Published in: Networked Systems

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Optimal Recoverable Mutual Exclusion Using only FASAS

next chapter On Verifying TSO Robustness for Event-Driven Asynchronous Programs

Available only for authorised users

Abdulla, P.A., Delzanno, G.: Parameterized verification. STTT 18(5), 469–473 (2016)CrossRef

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)MathSciNetCrossRef

Alberti, F., Ghilardi, S., Sharygina, N.: A framework for the verification of parameterized infinite-state systems. Fundam. Inform. 150(1), 1–24 (2017)MathSciNetCrossRef

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)

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)

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)

Bloem, R., et al.: Decidability of Parameterized Verification. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers, San Rafael (2015)

Bloem, R., et al.: Decidability in parameterized verification. SIGACT News 47(2), 53–64 (2016)MathSciNetCrossRef

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_55CrossRef

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)

11.

Delzanno, G.: Constraint-based verification of parameterized cache coherence protocols. Form. Methods Syst. Des. 23(3), 257–301 (2003)CrossRef

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)

13.

Delzanno, G.: A unified view of parameterized verification of abstract models of broadcast communication. STTT 18(5), 475–493 (2016)CrossRef

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_22CrossRef

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_30CrossRefMATH

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_15CrossRef

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_6CrossRef

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)

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_29CrossRef

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_11CrossRef

21.

http://alt-ergo.lri.fr

22.

http://functory.lri.fr/

23.

http://www.disi.unige.it/person/DelzannoG/MSR/

Title: Declarative Parameterized Verification of Topology-Sensitive Distributed Protocols
Authors: Sylvain Conchon
Giorgio Delzanno
Angelo Ferrando
Publisher: Springer International Publishing
Book: Networked Systems
Print ISBN: 978-3-030-05528-8

Electronic ISBN: 978-3-030-05529-5

Copyright Year: 2019
DOI: https://doi.org/10.1007/978-3-030-05529-5_14

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner