On Modelling and Analysing the Dynamic MANET On-Demand (DYMO) Routing Protocol

The Dynamic MANET On-demand (DYMO) routing protocol, being developed by the Internet Engineering Task Force, is a reactive routing protocol for mobile ad-hoc networks (MANETs). The basic operations of DYMO are route discovery and route maintenance. Constructing an analysable model of the DYMO protocol specification is a challenge because the routing operations are complex and the network topology changes dynamically. This paper presents a formal model of DYMO using Coloured Petri Nets. The model has a compact net structure, with functions in the arc inscriptions representing DYMO’s routing algorithms. The paper shows how careful crafting of the model results in smaller state spaces, compared with models using intuitively appealing hierarchical constructs. Initial results of state space analysis of the model are presented.

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

Access this chapter

Subscribe and save

Springer+ Basic €32.70 /Month

Buy Now

Price includes VAT (France)

eBook EUR 42.79 Price includes VAT (France)

Softcover Book EUR 52.74 Price includes VAT (France)

Tax calculation will be finalised at checkout

Purchases are for personal use only

Preview

Similar content being viewed by others

Uppaal vs Event-B for Modelling Optimised Link State Routing

Chapter © 2017

A Framework for Mobile Ad hoc Networks in Real-Time Maude

Chapter © 2014

A Tool for the Analysis of MANET Routing Protocols Based on Abstract State Machines

Chapter © 2021

References

  1. Basagni, S., Conti, M., Giordano, S., Stojmenovic, I.: Mobile Ad Hoc Networking. IEEE Press, New York (2004) BookGoogle Scholar
  2. Bhargavan, K., Obradovic, D., Gunter, C.A.: Formal Verification of Standards for Distance Vector Routing Protocols. JACM 49(4), 538–576 (2002) ArticleMathSciNetGoogle Scholar
  3. Cavalli, A., Grepet, C., Maag, S., Tortajada, V.: A Validation Model for the DSR Protocol. In: 24th International Conference on Distributed Computing Systems Workshops, pp. 768–773 (2004) Google Scholar
  4. Charkeres, I.D., Perkins, C.E.: Dynamic MANET On-demand (DYMO) Routing Protocol. IETF Internet Draft, draft-ietf-manet-dymo-10.txt (2007) Google Scholar
  5. Chiyangwa, S., Kwiatkowska, M.: A Timing Analysis of AODV. In: Steffen, M., Zavattaro, G. (eds.) FMOODS 2005. LNCS, vol. 3535, pp. 306–321. Springer, Heidelberg (2005) Google Scholar
  6. Clausen, T., Dearlove, C., Dean, J., Adjih, C.: Generalized MANET Packet/Message Format (2007), http://www.ietf.org/internet-drafts/draft-ietf-manet-packetbb-07.txt
  7. Design/CPN, http://www.daimi.au.dk/designCPN
  8. Espensen, K.L., Kjeldsen, M.K., Kristensen, L.M.: Towards Modelling and Verification of the DYMO Routing Protocol for Mobile Ad-hoc Networks. In: 8th Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools, Aarhus, Denmark, pp. 243–262 (2007) Google Scholar
  9. Espensen, K.L., Kjeldsen, M.K., Kristensen, L.M.: Modelling and Initial Validation of the DYMO Routing Protocol for Mobile Ad-Hoc Networks. In: van Hee, K.M., Valk, R. (eds.) PETRI NETS 2008. LNCS, vol. 5062, pp. 152–170. Springer, Heidelberg (2008) ChapterGoogle Scholar
  10. Gallasch, G.E., Billington, J.: A Parametric State Space for the Analysis of the Infinite Class of Stop-and-Wait Protocols. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 201–218. Springer, Heidelberg (2006) ChapterGoogle Scholar
  11. Gordon, M.J.C., Melham, T.F.: Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge (1993) MATHGoogle Scholar
  12. Holzmann, G.J.: The Spin Model Checker, Primer and Reference Manual. Addison-Wesley, Reading (2003) Google Scholar
  13. IETF. Mobile Ad-hoc Networks (manet), http://www.ietf.org/html.charters/manet-charter.html
  14. ITU-T. Recommendation Z.100: Specification and Description Language. International Telecomunication Union, Geneva (2007) Google Scholar
  15. Jensen, K.: Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use, vol. 1–3. Springer, Heidelberg (1997) MATHGoogle Scholar
  16. Jensen, K., Kristensen, L.M., Wells, L.: Coloured Petri Nets and CPN Tools for Modelling and Validation of Concurrent Systems. International Journal on Software Tools for Technology Transfer 9(3-4), 213–254 (2007) ArticleGoogle Scholar
  17. Johnson, D.B., Maltz, D.A., Hu, Y.C.: The Dynamic Source Routing Protocol for Mobile Ad hoc Networks (DSR). IETF MANET Working Group, draft-ietf-manet-dsr-09.txt (2003) Google Scholar
  18. Kristensen, L.M., Christensen, S., Jensen, K.: The Practitioner’s Guide to Coloured Petri Nets. International Journal on Software Tools for Technology Transfer 2(2), 98–132 (1998) ArticleMATHGoogle Scholar
  19. Larsen, K.G., Pettersson, P., Wang, Y.: UPPAAL in a Nutshell. International Journal on Software Tools for Technology Transfer 1(1-2), 134–152 (1997) ArticleMATHGoogle Scholar
  20. Obradovic, D.: Formal Analysis of Routing Protocols. PhD thesis, University of Pennsylvania (2002) Google Scholar
  21. Perkins, C.E.: Ad Hoc Networking. Addison-Wesley, Reading (2001) Google Scholar
  22. Perkins, C.E., Royer, E.M.: Ad-hoc On-demand Distance Vector Routing. In: 2nd IEEE Workshop on Mobile Computing Systems and Applications, New Orleans, Louisiana, USA, pp. 90–100 (1999) Google Scholar
  23. de Renesse, R., Aghvami, A.H.: Formal Verification of Ad-hoc Routing Protocols Using SPIN Model Checker. In: 12th IEEE Mediterranean Electrotechnical Conference, Dubrovnik, Croatia, Piscataway, N.J, vol. 3, pp. 1177–1182. IEEE, Los Alamitos (2004) ChapterGoogle Scholar
  24. Wibling, O., Parrow, J., Pears, A.: Automatized Verification of Ad Hoc Routing Protocols. In: de Frutos-Escrig, D., Núñez, M. (eds.) FORTE 2004. LNCS, vol. 3235, pp. 343–358. Springer, Heidelberg (2004) Google Scholar
  25. Xiong, C., Murata, T., Leigh, J.: An Approach for Verifying Routing Protocols in Mobile Ad Hoc Networks Using Petri Nets. In: Proceedings of IEEE 6th CAS Symposium on Emerging Technologies: Frontiers of Mobile and Wireless Communication, Shanghai, China, pp. 537–540 (2004) Google Scholar
  26. Xiong, C., Murata, T., Tsai, J.: Modeling and Simulation of Routing Protocol for Mobile Ad Hoc Wireless Networks Using Colored Petri Nets. In: Proceedings of Workshop on Formal Methods Applied to Defence Systems in Formal Methods in Software Engineering and Defence Systems, Conferences in Research and Practice in Information Technology, vol. 12, pp. 145–153 (2002) Google Scholar
  27. Yuan, C., Billington, J.: A Coloured Petri Net Model of the Dynamic MANET On-demand Routing Protocol. In: 7th Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools, Department of Computer Science Technical Report, DAIMI PB 579, Aarhus, Denmark, pp. 37–56 (2006) Google Scholar
  28. Yuan, C., Billington, J.: On Modelling the Dynamic MANET On-demand (DYMO) Routing Protocol. In: International Workshop on Petri Nets and Distributed Systems (PNDS 2008), Xi’an, China, pp. 47–66 (2008) Google Scholar

Author information

Authors and Affiliations

  1. Computer Systems Engineering Centre, University of South Australia, Mawson Lakes Campus, SA, 5095, Australia Jonathan Billington & Cong Yuan
  1. Jonathan Billington
You can also search for this author in PubMed Google Scholar You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Faculty of Science, Department of Computer Science, University of Aarhus, IT-parken, Aabogade 34, 8200, Aarhus N, Denmark Kurt Jensen
  2. School of Electrical and Information Engineering, University of South Australia, Mawson Lakes Campus, 5095, Mawson Lakes, South Australia, Australia Jonathan Billington
  3. SCS, Newcastle University, NE1 7RU, Newcastle upon Tyne, UK Maciej Koutny

Rights and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Billington, J., Yuan, C. (2009). On Modelling and Analysing the Dynamic MANET On-Demand (DYMO) Routing Protocol. In: Jensen, K., Billington, J., Koutny, M. (eds) Transactions on Petri Nets and Other Models of Concurrency III. Lecture Notes in Computer Science, vol 5800. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04856-2_5

Download citation

Share this chapter

Anyone you share the following link with will be able to read this content:

Get shareable link

Sorry, a shareable link is not currently available for this article.

Copy to clipboard

Provided by the Springer Nature SharedIt content-sharing initiative