Skip to main content
SpringerLink
Log in

Parameterized Verification and Model Checking for Distributed Broadcast Protocols

  • Conference paper
Graph Transformation (ICGT 2014)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 8571))

Included in the following conference series:

  • 652 Accesses

Abstract

We report on recent research lines related to parameterized verification and model checking applied to formal models of distributed algorithms. Both approaches are based on graph rewriting and graph transformation systems. Case-studies include distributed mutual exclusion protocols like Ricart-Agrawala, routing protocols like link reversal, and distributed consensus protocols like Paxos. Verification algorithms for restricted classes of models exploit finite-state abstractions, symbolic representations based on graph orderings, the theory of well-structured transition systems, and reachability algorithms based on labeling procedures.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abdulla, P., Delzanno, G.: Constrained multiset rewriting. In: AVIS 2006 (2006)

    Google Scholar 

  2. Abdulla, P.A., Atig, M.F., Rezine, O.: Verification of directed acyclic ad hoc networks. In: Beyer, D., Boreale, M. (eds.) FMOODS/FORTE 2013. LNCS, vol. 7892, pp. 193–208. Springer, Heidelberg (2013)

    Google Scholar 

  3. Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.-K.: General decidability theorems for infinite-state systems. In: LICS 1996, pp. 313–321. IEEE Computer Society (1996)

    Google Scholar 

  4. Abdulla, P.A., Delzanno, G., Van Begin, L.: A classification of the expressive power of well-structured transition systems. Inf. Comput. 209(3), 248–279 (2011)

    Article  MATH  Google Scholar 

  5. Abdulla, P.A., Delzanno, G., Rezine, A.: Automatic verification of directory-based consistency protocols with graph constraints. Int. J. Found. Comput. Sci. 22(4) (2011)

    Google Scholar 

  6. Abdulla, P.A., Delzanno, G., Rezine, A.: Approximated parameterized verification of infinite-state processes with global conditions. Formal Methods in System Design 34(2), 126–156 (2009)

    Article  MATH  Google Scholar 

  7. Abdulla, P.A., Delzanno, G., Rezine, O., Sangnier, A., Traverso, R.: On the verification of timed ad hoc networks. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol. 6919, pp. 256–270. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  8. Abdulla, P.A., Ben Henda, N., Delzanno, G., Rezine, A.: Handling parameterized systems with non-atomic global conditions. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol. 4905, pp. 22–36. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  9. Abdulla, P.A., Jonsson, B.: Undecidable verification problems for programs with unreliable channels. Inf. Comput. 130(1), 71–90 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  10. Abdulla, P.A., Jonsson, B.: Ensuring completeness of symbolic verification methods for infinite-state systems. Theor. Comput. Sci. 256(1-2), 145–167 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  11. Abdulla, P.A., Nylén, A.: Better is better than well: On efficient verification of infinite-state systems. In: LICS 2000, pp. 132–140. IEEE Computer Society (2000)

    Google Scholar 

  12. Alberti, F., Ghilardi, S., Pagani, E., Ranise, S., Rossi, G.P.: Automated support for the design and validation of fault tolerant parameterized systems: A case study. ECEASST 35 (2010)

    Google Scholar 

  13. 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, pp. 101–116 (2012)

    Google Scholar 

  14. Bertrand, N., Fournier, P., Sangnier, A.: Playing with probabilities in reconfigurable broadcast networks. In: Muscholl, A. (ed.) FOSSACS 2014 (ETAPS). LNCS, vol. 8412, pp. 134–148. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  15. Bokor, P., Serafini, M., Suri, N.: On efficient models for model checking message-passing distributed protocols. In: Hatcliff, J., Zucca, E. (eds.) FMOODS 2010, Part II. LNCS, vol. 6117, pp. 216–223. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  16. Danos, V., Laneve, C.: Formal molecular biology. Theor. Comput. Sci. 325(1), 69–110 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  17. Delzanno, G.: An overview of msr(c): A clp-based framework for the symbolic verification of parameterized concurrent systems. Electr. Notes Theor. Comput. Sci. 76, 65–82 (2002)

    Article  Google Scholar 

  18. Delzanno, G.: Constraint-based verification of parameterized cache coherence protocols. FMSD 23(3), 257–301 (2003)

    MATH  Google Scholar 

  19. Delzanno, G.: Constraint-based automatic verification of abstract models of multithreaded programs. TPLP 7(1-2), 67–91 (2007)

    MATH  MathSciNet  Google Scholar 

  20. Delzanno, G., Esparza, J., Podelski, A.: Constraint-based analysis of broadcast protocols. In: Flum, J., Rodríguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol. 1683, pp. 50–66. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  21. Delzanno, G., Di Giusto, C., Gabbrielli, M., Laneve, C., Zavattaro, G.: The κ-lattice: Decidability boundaries for qualitative analysis in biological languages. In: Degano, P., Gorrieri, R. (eds.) CMSB 2009. LNCS, vol. 5688, pp. 158–172. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  22. Delzanno, G., Rensink, A., Traverso, R.: Graph- versus vector-based analysis of a consensus protocol. In: GRAPHITE (2014)

    Google Scholar 

  23. Delzanno, G., Rezine, A.: A lightweight regular model checking approach for parameterized systems. STTT 14(2), 207–222 (2012)

    Article  Google Scholar 

  24. Delzanno, G., Rosa-Velardo, F.: On the coverability and reachability languages of monotonic extensions of petri nets. Theor. Comput. Sci. 467, 12–29 (2013)

    Article  MATH  MathSciNet  Google Scholar 

  25. Delzanno, G., Sangnier, A., Traverso, R.: Parameterized verification of broadcast networks of register automata. In: Abdulla, P.A., Potapov, I. (eds.) RP 2013. LNCS, vol. 8169, pp. 109–121. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  26. Delzanno, G., Sangnier, A., Traverso, R., Zavattaro, G.: On the complexity of parameterized reachability in reconfigurable broadcast networks. In: FSTTCS 2012. LIPIcs, vol. 18, pp. 289–300. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2012)

    Google Scholar 

  27. 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)

    Chapter  Google Scholar 

  28. 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)

    Chapter  Google Scholar 

  29. 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)

    Google Scholar 

  30. Delzanno, G., Traverso, R.: Decidability and complexity results for verification of asynchronous broadcast networks. In: Dediu, A.-H., Martín-Vide, C., Truthe, B. (eds.) LATA 2013. LNCS, vol. 7810, pp. 238–249. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  31. Ding, G.: Subgraphs and well quasi ordering. J. of Graph Theory 16(5), 489–502 (1992)

    Article  MATH  Google Scholar 

  32. Emerson, E.A., Namjoshi, K.S.: On model checking for non-deterministic infinite-state systems. In: LICS 1998, pp. 70–80. IEEE Computer Society (1998)

    Google Scholar 

  33. Ene, C., Muntean, T.: A broadcast-based calculus for communicating systems. In: IPDPS 2001, p. 149. IEEE Computer Society (2001)

    Google Scholar 

  34. Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In: LICS 1999, pp. 352–359. IEEE Computer Society (1999)

    Google Scholar 

  35. Fehnker, A., van Glabbeek, R., Höfner, P., McIver, A., Portmann, M., Tan, W.L.: Automated analysis of AODV using UPPAAL. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 173–187. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  36. Fehnker, A., van Glabbeek, R., Höfner, P., McIver, A., Portmann, M., Tan, W.L.: A process algebra for wireless mesh networks. In: Seidl, H. (ed.) ESOP. LNCS, vol. 7211, pp. 295–315. Springer, Heidelberg (2012)

    Google Scholar 

  37. Fehnker, A., van Hoesel, L., Mader, A.: Modelling and verification of the lmac protocol for wireless sensor networks. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol. 4591, pp. 253–272. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  38. Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theor. Comput. Sci. 256(1-2), 63–92 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  39. Fischer, M.J., Lynch, N.A., Paterson, M.: Impossibility of distributed consensus with one faulty process. J. ACM 32(2), 374–382 (1985)

    Article  MATH  MathSciNet  Google Scholar 

  40. Függer, M., Widder, J.: Efficient checking of link-reversal-based concurrent systems. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 486–499. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  41. German, S.M., Sistla, A.P.: Reasoning about systems with many processes. J. ACM 39(3), 675–735 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  42. Ghamarian, A.H., de Mol, M., Rensink, A., Zambon, E., Zimakova, M.: Modelling and analysis using groove. STTT 14(1), 15–40 (2012)

    Article  Google Scholar 

  43. Holzmann, G.J.: The SPIN Model Checker - primer and reference manual. Addison-Wesley (2004)

    Google Scholar 

  44. John, A., Konnov, I., Schmid, U., Veith, H., Widder, J.: Towards modeling and model checking fault-tolerant distributed algorithms. In: Bartocci, E., Ramakrishnan, C.R. (eds.) SPIN 2013. LNCS, vol. 7976, pp. 209–226. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  45. John, A., Konnov, I., Schmid, U., Veith, H., Widder, J.: Towards modeling and model checking fault-tolerant distributed algorithms. In: Bartocci, E., Ramakrishnan, C.R. (eds.) SPIN 2013. LNCS, vol. 7976, pp. 209–226. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  46. Joshi, S., König, B.: Applying the graph minor theorem to the verification of graph transformation systems. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 214–226. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  47. Kaminski, M., Francez, N.: Finite-memory automata. Theor. Comput. Sci. 134(2), 329–363 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  48. Konnov, I., Veith, H., Widder, J.: Who is afraid of model checking distributed algorithms? In: Unpublished Contribution to: CAV Workshop (EC)2 (2012)

    Google Scholar 

  49. Lamport, L.: The part-time parliament. ACM Transactions on Computer Systems 16(3), 133–169 (1998)

    Article  Google Scholar 

  50. Marzullo, K., Mei, A., Meling, H.: A simpler proof for paxos and fast paxos. Course Notes (2013)

    Google Scholar 

  51. 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)

    Chapter  Google Scholar 

  52. Saksena, M., Wibling, O., Jonsson, B.: Graph grammar modeling and verification of ad hoc routing protocols. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. TACAS, pp. 18–32. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  53. Schnoebelen, P.: Revisiting ackermann-hardness for lossy counter machines and reset petri nets. In: Hliněný, P., Kučera, A. (eds.) MFCS 2010. LNCS, vol. 6281, pp. 616–628. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  54. Singh, A., Ramakrishnan, C.R., Smolka, S.A.: Query-based model checking of ad hoc network protocols. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 603–619. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  55. Singh, A., Ramakrishnan, C.R., Smolka, S.A.: A process calculus for mobile ad hoc networks. Sci. Comput. Program. 75(6), 440–469 (2010)

    Article  MATH  MathSciNet  Google Scholar 

  56. Traverso, R.: Formal verification of ad hoc networks. PhD thesis, University of Genova (2014)

    Google Scholar 

  57. Tsuchiya, T., Schiper, A.: Using bounded model checking to verify consensus algorithms. In: Taubenfeld, G. (ed.) DISC 2008. LNCS, vol. 5218, pp. 466–480. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. DIBRIS, Università di Genova, Italy

    Giorgio Delzanno

Authors
  1. Giorgio Delzanno
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Hasso Plattner Institut an der Universität Potsdam, Prof.-Dr.-Helmert-Strasse 2-3, 14482, Potsdam, Germany

    Holger Giese

  2. Fakultät für Ingenieurwissenschaften, Abteilung für Informatik und Angewandte Kognitionswissenscaft, Universität Duisburg-Essen, Lotharstraße 65, 47057, Duisburg, Germany

    Barbara König

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Delzanno, G. (2014). Parameterized Verification and Model Checking for Distributed Broadcast Protocols. In: Giese, H., König, B. (eds) Graph Transformation. ICGT 2014. Lecture Notes in Computer Science, vol 8571. Springer, Cham. https://doi.org/10.1007/978-3-319-09108-2_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-09108-2_1

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-09107-5

  • Online ISBN: 978-3-319-09108-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation