Advertisement

Abstract

We formulate a method to compute global invariants of dynamic process networks. In these networks, inter-process connectivity may be altered by an adversary at any point in time. Dynamic networks serve as models for ad-hoc and sensor-network protocols. The analysis combines elements of compositional reasoning, symmetry reduction, and abstraction. Together, they allow a small “cutoff” network to represent arbitrarily large networks. A compositional invariant computed on the small network generalizes to a parametric invariant of the shape “for all networks and all processes: property p holds of each process and its local neighborhood.” We illustrate this method by showing how to compute useful invariants for a simple dining philosophers protocol, and the latest version of the ad-hoc routing protocol AODV (version 2).

Keywords

Model Check Dynamic Network Local Symmetry Symmetry Reduction Ring Network 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    Ad Hoc On-Demand Distance Vector (AODV) Routing. Internet Draft, IETF Mobile Ad hoc Networks Working GroupGoogle Scholar
  2. 2.
    Dynamic MANET On-demand (AODVv2) Routing. Internet Draft, IETF Mobile Ad hoc Networks Working Group, http://datatracker.ietf.org/doc/draft-ietf-manet-aodvv2/
  3. 3.
    Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.-K.: General decidability theorems for infinite-state systems. In: LICS, pp. 313–321. IEEE Computer Society (1996)Google Scholar
  4. 4.
    Abdulla, P.A., Haziza, F., Holík, L.: All for the price of few. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 476–495. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  5. 5.
    Apt, K.R., Kozen, D.: Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett. 22(6), 307–309 (1986)CrossRefMathSciNetGoogle Scholar
  6. 6.
    Bhargavan, K., Obradovic, D., Gunter, C.A.: Formal verification of standards for distance vector routing protocols. J. ACM 49(4), 538–576 (2002)CrossRefMathSciNetGoogle Scholar
  7. 7.
    Bouajjani, A., Jurski, Y., Sighireanu, M.: A generic framework for reasoning about dynamic networks of infinite-state processes. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 690–705. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  8. 8.
    Clarke, E.M., Talupur, M., Veith, H.: Environment abstraction for parameterized verification. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 126–141. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  9. 9.
    Cousot, P., Cousot, R.: Automatic synthesis of optimal invariant assertions: mathematical foundations. In: ACM Symposium on Artificial Intelligence & Programming Languages, vol. 12(8), pp. 1–12. ACM, Rochester (1977)Google Scholar
  10. 10.
    Das, S., Dill, D.L.: Counter-example based predicate discovery in predicate abstraction. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, pp. 19–32. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  11. 11.
    de Roever, W.-P., de Boer, F., Hannemann, U., Hooman, J., Lakhnech, Y., Poel, M., Zwiers, J.: Concurrency Verification: Introduction to Compositional and Noncompositional Proof Methods. Cambridge University Press (2001)Google Scholar
  12. 12.
    Delzanno, G., Sangnier, A., Traverso, R., Zavattaro, G.: On the complexity of parameterized reachability in reconfigurable broadcast networks. In: FSTTCS. LIPIcs, vol. 18, pp. 289–300. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2012)Google Scholar
  13. 13.
    Delzanno, G., Sangnier, A., Zavattaro, G.: Parameterized verification of safety properties in ad hoc network protocols. In: PACO. EPTCS, vol. 60, pp. 56–65 (2011)Google Scholar
  14. 14.
    Delzanno, G., Sangnier, A., Zavattaro, G.: Verification of ad hoc networks with node and communication failures. In: Giese, H., Rosu, G. (eds.) FORTE 2012 and FMOODS 2012. LNCS, vol. 7273, pp. 235–250. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  15. 15.
    Dijkstra, E., Scholten, C.: Predicate Calculus and Program Semantics. Springer (1990)Google Scholar
  16. 16.
    Emerson, E., Namjoshi, K.: Reasoning about rings. In: ACM Symposium on Principles of Programming Languages (1995)Google Scholar
  17. 17.
    Emerson, E.A., Trefler, R.J., Wahl, T.: Reducing model checking of the few to the one. In: Liu, Z., Kleinberg, R.D. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 94–113. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  18. 18.
    German, S., Sistla, A.: Reasoning about systems with many processes. Journal of the ACM (1992)Google Scholar
  19. 19.
    Höfner, P., van Glabbeek, R.J., Tan, W.L., Portmann, M., McIver, A., Fehnker, A.: A rigorous analysis of aodv and its variants. In: MSWiM, pp. 203–212. ACM (2012)Google Scholar
  20. 20.
    Kesten, Y., Maler, O., Marcus, M., Pnueli, A., Shahar, E.: Symbolic model checking with rich ssertional languages. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 424–435. Springer, Heidelberg (1997)Google Scholar
  21. 21.
    Langari, Z., Trefler, R.: Symmetry for the analysis of dynamic systems. In: NASA Formal Methods 2011, pp. 252–266 (2011)Google Scholar
  22. 22.
    Namjoshi, K.S.: Symmetry and completeness in the analysis of parameterized systems. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 299–313. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  23. 23.
    Namjoshi, K.S., Trefler, R.J.: Local symmetry and compositional verification. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 348–362. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  24. 24.
    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)CrossRefGoogle Scholar
  25. 25.
    Owicki, S.S., Gries, D.: Verifying properties of parallel programs: An axiomatic approach. Commun. ACM 19(5), 279–285 (1976)CrossRefzbMATHMathSciNetGoogle Scholar
  26. 26.
    Pnueli, A., Ruah, S., Zuck, L.D.: Automatic deductive verification with invisible invariants. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 82–97. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  27. 27.
    Saksena, M., Wibling, O., Jonsson, B.: Graph grammar modelling and verification of ad hoc routing protocols. LNCS, pp. 18–32 (2008)Google Scholar
  28. 28.
    Shtadler, Z., Grumberg, O.: Network grammars, communication behaviors and automatic verification. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 151–165. Springer, Heidelberg (1990)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2015

Authors and Affiliations

  1. 1.Bell LaboratoriesAlcatel-LucentMurray HillUSA
  2. 2.University of WaterlooWaterlooCanada

Personalised recommendations