Automatized Verification of Ad Hoc Routing Protocols

  • Oskar Wibling
  • Joachim Parrow
  • Arnold Pears
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3235)


Numerous specialized ad hoc routing protocols are currently proposed for use, or being implemented. Few of them have been subjected to formal verification. This paper evaluates two model checking tools, SPIN and UPPAAL, using the verification of the Lightweight Underlay Network Ad hoc Routing protocol (LUNAR) as a case study. Insights are reported in terms of identifying important modeling considerations and the types of ad hoc protocol properties that can realistically be verified.


Mobile ad hoc networks routing protocols formal verification model checking SPIN UPPAAL LUNAR 


  1. 1.
    Barnat, J., Brim, L., Stribrna, J.: Distributed LTL model-checking in SPIN. Technical report, Masaryk University (December 2000)Google Scholar
  2. 2.
    Behrmann, G., Hune, T., Vaandrager, F.: Distributed timed model checking - how the search order matters. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, Springer, Heidelberg (2000)CrossRefGoogle Scholar
  3. 3.
    Chiyangwa, S., Kwiatkowska, M.: Analysing timed properties of AODV with UPPAAL. Technical report, University of Birmingham, Technical Report CSR-04-4 (March 2004)Google Scholar
  4. 4.
    Clausen, T., Jacquet, P.: Request for Comments: Optimized link state routing protocol (OLSR) (October 2003),
  5. 5.
    Das, S., Dill, D.L.: Counter-example based predicate discovery in predicate abstraction. In: Formal Methods in Computer-Aided Design, November 2002, Springer, Heidelberg (2002)Google Scholar
  6. 6.
    Engler, D., Musuvathi, M.: Static analysis versus software model checking for bug finding. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 191–210. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  7. 7.
    Holzmann, G.J.: The Spin Model Checker, Primer and Reference Manual. Addison-Wesley, Reading (2003)Google Scholar
  8. 8.
    Holzmann, G.J., Peled, D.: An improvement in formal verification. In: Proc. FORTE Conference (1994)Google Scholar
  9. 9.
    IETF MANET Working Group. MANET charter (2004),
  10. 10.
    Information Sciences Institute. The network simulator – ns-2 home page (2004),
  11. 11.
    Johnson, D.B.: Routing in ad hoc networks of mobile hosts. In: Proc. IEEE Workshop on Mobile Computing Systems and Applications, December 1994, pp. 158–163 (1994)Google Scholar
  12. 12.
    Johnson, D.B., Maltz, D.A., Hu, Y.-C.: Internet draft: The dynamic source routing protocol for mobile ad hoc networks (DSR) (April 2003),
  13. 13.
    Kwiatkowska, M., Norman, G., Sproston, J.: Probabilistic model checking of the IEEE 802.11 wireless local area network protocol. In: Proc. Second Joint International Workshop on Process Algebra and Probabilistic Methods, Performance Modeling and Verification, July 2002, pp. 169–187 (2002)Google Scholar
  14. 14.
    Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: Efficient verification of real-time systems: Compact data structures and state-space reduction. In: Proc. 18th IEEE Real-Time Systems Symposium (RTSS), December 1997, pp. 14–24 (1997)Google Scholar
  15. 15.
    Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a Nutshell. Int. Journal on Software Tools for Technology Transfer 1(1–2), 134–152 (1997)CrossRefzbMATHGoogle Scholar
  16. 16.
    Lundgren, H.: Implementation and Real-world Evaluation of Routing Protocols for Wireless Ad hoc Networks. Licentiate thesis, Uppsala University (2002)Google Scholar
  17. 17.
    Lundgren, H., Lundberg, D., Nielsen, J., Nordström, E., Tschudin, C.: A large-scale testbed for reproducible ad hoc protocol evaluations. In: Proc. 3rd annual IEEE Wireless Communications and Networking Conference (WCNC), March 2002, pp. 412–418. IEEE, Los Alamitos (2002)Google Scholar
  18. 18.
    Obradovic, D.: Formal Analysis of Routing Protocols. Phd thesis, University of Pennsylvania (2002)Google Scholar
  19. 19.
    Ogier, R., Templin, F., Lewis, M.: Internet draft: Topology dissemination based on reverse-path forwarding (TBRPF) (October 2003),
  20. 20.
    Perkins, C., Belding-Royer, E., Das, S.: Request for Comments: Ad hoc ondemand distance vector (AODV) routing (July 2003),
  21. 21.
    Perkins, C.E., Royer, E.M.: Ad hoc on-demand distance vector routing. In: Proc. 2nd IEEE Workshop on Mobile Computing Systems and Applications, February 1999, pp. 90–100 (1999)Google Scholar
  22. 22.
    Ruys, T.C.: Towards Effective Model Checking. Phd thesis, University of Twente (March 2001)Google Scholar
  23. 23.
    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 (2004)Google Scholar
  24. 24.
    University of Cambridge Computer Laboratory. Automated reasoning group HOL page (2004),
  25. 25.
    Uppsala University and Aalborg University. UPPAAL home page (2004),
  26. 26.
    Verinet group. Verinet home page (2004),
  27. 27.
    Oskar Wibling. LUNAR pseudo code description (2004),
  28. 28.
    Wikipedia. Ad hoc protocol list (2004),
  29. 29.
    Xiong, C., Murata, T., Tsai, J.: Modelling and simulation of routing protocol for mobile ad hoc networks using coloured Petri nets. In: Proc. Workshop on Formal Methods Applied to Defence Systems in Formal Methods in Software Engineering and Defence Systems (2002)Google Scholar

Copyright information

© IFIP International Federation for Information Processing 2004

Authors and Affiliations

  • Oskar Wibling
    • 1
  • Joachim Parrow
    • 1
  • Arnold Pears
    • 1
  1. 1.Department of Information TechnologyUppsala UniversityUppsalaSweden

Personalised recommendations