Skip to main content
SpringerLink
Log in
Book cover

Transactions on Petri Nets and Other Models of Concurrency III pp 98–126Cite as

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

  • Chapter

Part of the book series: Lecture Notes in Computer Science ((TOPNOC,volume 5800))

Abstract

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.

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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Basagni, S., Conti, M., Giordano, S., Stojmenovic, I.: Mobile Ad Hoc Networking. IEEE Press, New York (2004)

    Book  Google Scholar 

  2. Bhargavan, K., Obradovic, D., Gunter, C.A.: Formal Verification of Standards for Distance Vector Routing Protocols. JACM 49(4), 538–576 (2002)

    Article  MathSciNet  Google 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)

    Chapter  Google 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)

    Chapter  Google 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)

    MATH  Google 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)

    MATH  Google 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)

    Article  Google 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)

    Article  MATH  Google 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)

    Article  MATH  Google 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)

    Chapter  Google 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 

Download references

Author information

Authors and Affiliations

  1. Computer Systems Engineering Centre, University of South Australia, Mawson Lakes Campus, SA, 5095, Australia

    Jonathan Billington & Cong Yuan

Authors
  1. Jonathan Billington
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Cong Yuan
    View author publications

    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

Reprints 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

  • DOI: https://doi.org/10.1007/978-3-642-04856-2_5

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-04854-8

  • Online ISBN: 978-3-642-04856-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation