Advertisement

Graph Grammar Modeling and Verification of Ad Hoc Routing Protocols

  • Mayank Saksena
  • Oskar Wibling
  • Bengt Jonsson
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4963)

Abstract

We present a technique for modeling and automatic verification of network protocols, based on graph transformation. It is suitable for protocols with a potentially unbounded number of nodes, in which the structure and topology of the network is a central aspect, such as routing protocols for ad hoc networks. Safety properties are specified as a set of undesirable global configurations. We verify that there is no undesirable configuration which is reachable from an initial configuration, by means of symbolic backward reachability analysis.

In general, the reachability problem is undecidable. We implement the technique in a graph grammar analysis tool, and automatically verify several interesting nontrivial examples. Notably, we prove loop freedom for the DYMO ad hoc routing protocol. DYMO is currently on the IETF standards track, to potentially become an Internet standard.

Keywords

Network Node Graph Transformation Route Request Graph Grammar Reachability Analysis 
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.
    Abdulla, P.A., Delzanno, G., Rezine, A., Ben Henda, N.: Regular model checking without transducers (On Efficient Verification of Parameterized Systems). In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 721–736. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  2. 2.
    Abdulla, P.A., Čerāns, K., Jonsson, B., Yih-Kuen, T.: Algorithmic analysis of programs with well quasi-ordered domains. Information and Computation 160, 109–127 (2000)zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    Abdulla, P.A., Jonsson, B.: Verifying programs with unreliable channels. Information and Computation 127(2), 91–101 (1996)zbMATHCrossRefMathSciNetGoogle Scholar
  4. 4.
    Abolhasan, M., Wysocki, T., Dutkiewicz, E.: A review of routing protocols for mobile ad hoc networks. Ad Hoc Networks 2(1), 1–22 (2004)CrossRefGoogle Scholar
  5. 5.
    Bauer, J.: Analysis of Communication Topologies by Partner Abstraction. PhD thesis, Universität des Saarlandes (2006)Google Scholar
  6. 6.
    Bauer, J., Wilhelm, R.: Static Analysis of Dynamic Communication Systems. In: 14th International Static Analysis Symposium, Springer, Heidelberg (2007)Google Scholar
  7. 7.
    Becker, B., Beyer, D., Giese, H., Klein, F., Schilling, D.: Symbolic invariant verification for systems with dynamic structural adaptation. In: Proc. ICSE 2006, 28th Int. Conf. on Software Engineering, pp. 72–81. ACM Press, New York (2006)CrossRefGoogle Scholar
  8. 8.
    Bhargavan, K., Obradovic, D., Gunter, C.A.: Formal verification of standards for distance vector routing protocols. Journal of the ACM 49(4), 538–576 (2002)CrossRefMathSciNetGoogle Scholar
  9. 9.
    Broch, J., Maltz, D.A., Johnson, D.B., Hu, Y.-C., Jetcheva, J.: A performance comparison of multi-hop wireless ad hoc network routing protocols. In: Proceedings of MobiCom 1998 (October 1998)Google Scholar
  10. 10.
    Chakeres, I.D., Perkins, C.E.: DYMO - Dynamic MANET On-demand Routing Protocol home page (2007), http://www.ianchak.com/dymo/
  11. 11.
    Chakeres, I.D., Perkins, C.E.: Dynamic MANET On-demand (DYMO) Routing. In: Internet draft, draft-ietf-manet-dymo-10.txt (July 2007)Google Scholar
  12. 12.
    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)Google Scholar
  13. 13.
    Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In: Proc. LICS 1999 14th IEEE Int. Symp. on Logic in Computer Science (1999)Google Scholar
  14. 14.
    GBT - Graph Backwards Tool project home page. http://www.it.uu.se/research/group/mobility/adhoc/gbt
  15. 15.
    Holzmann, G.: The model checker SPIN. IEEE Trans. on Software Engineering SE-23(5), 279–295 (1997)CrossRefMathSciNetGoogle Scholar
  16. 16.
    Johnson, D.B., Maltz, D.A., Broch, J.: DSR: The dynamic source routing protocol for multi-hop wireless ad hoc networks. In: Ad Hoc Networking, ch. 5, pp. 139–172. Addison-Wesley, Reading (2001)Google Scholar
  17. 17.
    Jonsson, B., Kempe, L.: Verifying safety properties of a class of infinite-state distributed algorithms. In: Wolper, P. (ed.) CAV 1995. LNCS, vol. 939, pp. 42–53. Springer, Heidelberg (1995)Google Scholar
  18. 18.
    Kastenberg, H., Rensink, A.: Model checking dynamic states in GROOVE. In: SPIN Workshop, pp. 299–305. Springer, Heidelberg (2006)Google Scholar
  19. 19.
    König, B., Kozioura, V.: Counterexample-guided abstraction refinement for the analysis of graph transformation systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 197–211. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  20. 20.
    List of ad-hoc routing protocols - Wikipedia, the free encyclopedia, http://en.wikipedia.org/wiki/Ad_hoc_routing_protocol_list
  21. 21.
    Perkins, C.E., Belding-Royer, E.M.: Ad-hoc on-demand distance vector routing. In: Proc. 2nd Workshop on Mobile Computing Systems and Applications (WMCSA 1999), pp. 90–100. IEEE Computer Society Press, Los Alamitos (1999)Google Scholar
  22. 22.
    Saksena, M., Wibling, O., Jonsson, B.: Graph grammar modeling and verification of ad hoc routing protocols. Technical Report 2007-035, Dept. of Information Technology, Uppsala University, Sweden (2007)Google Scholar
  23. 23.
    The official IETF MANET working group web page, http://www.ietf.org/html.charters/manet-charter.html
  24. 24.
    Tschudin, C., Gold, R., Rensfelt, O., Wibling, O.: LUNAR: a lightweight underlay network ad-hoc routing protocol and implementation. In: Proc. Next Generation Teletraffic and Wired/Wireless Advanced Networking (NEW2AN) (February 2004)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Mayank Saksena
    • 1
  • Oskar Wibling
    • 1
  • Bengt Jonsson
    • 1
  1. 1.Dept. of Information Technology UppsalaSweden

Personalised recommendations