Advertisement

Specification and Validation of an Edge Router Discovery Protocol for Mobile Ad Hoc Networks

  • Lars Michael Kristensen
  • Kurt Jensen
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3147)

Abstract

We present an industrial project at Ericsson Telebit A/S where Coloured Petri Nets (CP-nets or CPNs) have been used for the design and specification of an edge router discovery protocol for mobile ad-hoc networks. The Edge Router Discovery Protocol (ERDP) supports an edge router in a stationary core network in assigning network address prefixes to gateways in mobile ad-hoc networks. This paper focuses on how CP-nets and the CPN computer tools have been applied in the development of ERDP. A CPN model has been constructed that constitutes a formal executable specification of ERDP. Simulation and message sequence charts were used for initial investigations of the protocol’s behaviour. Then state space analysis was applied to conduct a formal verification of the key properties of ERDP. Both the modelling, simulation, and subsequent state space analysis helped in identifying several omissions and errors in the design, demonstrating the benefits of using formal modelling and analysis in a protocol design process.

Keywords

Edge Router IPv6 Address Strongly Connect Component Router Advertisement State Space Method 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Christensen, S.: Message Sequence Charts. User’s Manual (January 1997), Available via http://www.daimi.au.dk/designCPN
  2. 2.
    Christensen, S., Kristensen, L.M., Mailund, T.: A Sweep-Line Method for State Space Exploration. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 450–464. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  3. 3.
    Clarke, E.M., Wing, J.M.: Formal Methods: State of the Art and Future Directions. ACM Computing Surveys 28(4), 626–643 (1996)CrossRefGoogle Scholar
  4. 4.
    Conta and S. Deering. Internet Control Message Protocol (ICMPv6) for the Internet Protocol Version 6 (IPV6) Specification, RFC 2463 (December 1998) (work in progress)Google Scholar
  5. 5.
  6. 6.
    The CPN Group at University of Aarhus, http://www.daimi.au.dk/CPnets
  7. 7.
    Deering, S., Hinden, R.: Internet Protocol, Version 6 (IPV6) Specification, RFC 2460 (December 1998) (work in progress)Google Scholar
  8. 8.
    Desel, J.: Basic Linear Algebraic Techniques for Place/Transition Nets. In: Reisig, W., Rozenberg, G. (eds.) APN 1998. LNCS, vol. 1491, pp. 257–308. Springer, Heidelberg (1998)Google Scholar
  9. 9.
    Desel, J.: Validation of Process Models by Construction of Process Nets. In: van der Aalst, W.M.P., Desel, J., Oberweis, A. (eds.) Business Process Management. LNCS, vol. 1806, pp. 110–128. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  10. 10.
    Desel, J., Reisig, W.: Place/Transition Petri Nets. In: Reisig, W., Rozenberg, G. (eds.) APN 1998. LNCS, vol. 1491, pp. 122–173. Springer, Heidelberg (1998)Google Scholar
  11. 11.
  12. 12.
    Ericsson Telebit A/S, http://www.tbit.dk
  13. 13.
    Esparza, J.: Model Checking using Net Unfoldings. Science of Computer Programming 23, 151–195 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  14. 14.
    Internet Engineering Task Force. Mobile ad-hoc networks, http://www.ietf.org/html.charters/manet-charter.html
  15. 15.
    Huitema, C.: IPv6: The New Internet Protocol. Prentice-Hall, Englewood Cliffs (1998)Google Scholar
  16. 16.
    Examples of Industrial Use of CP-nets, http://www.daimi.au.dk/CPnets/intro/example_indu.html
  17. 17.
    The Internet Engineering Task Force, http://www.ietf.org
  18. 18.
    Jensen, K.: Coloured Petri Nets - Basic Concepts, Analysis Methods and Practical Use, vol. 1-3. Springer, Heidelberg (1997)zbMATHGoogle Scholar
  19. 19.
    Jensen, K.: Condensed State Spaces for Symmetrical Coloured Petri Nets. Formal Methods in System Design 9(1/2), 7–40 (1996)CrossRefGoogle Scholar
  20. 20.
    Kristensen, L.M.: Ad-hoc Networking and IPv6: Modelling and Validation, http://www.pervasive.dk/projects/IPv6/IPv6_summary
  21. 21.
    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)zbMATHCrossRefGoogle Scholar
  22. 22.
    Narten, T., Nordmark, E., Simpson, W.: Neighbor Discovery for IP Version 6 (IPv6), RFC 2461 (December 1998) (work in progress)Google Scholar
  23. 23.
    Perkins, C.E.: Ad Hoc Networking. Addison-Wesley, Reading (2001)Google Scholar
  24. 24.
    Rasmussen, J.L., Singh, M.: Designing a Security System by Means of Coloured Petri Nets. In: Billington, J., Reisig, W. (eds.) ICATPN 1996. LNCS, vol. 1091, pp. 400–419. Springer, Heidelberg (1996)Google Scholar
  25. 25.
    Reisig, W.: Petri Nets. EACTS Monographs in Theoretical Computer Science, vol. 4. Springer, Heidelberg (1985)zbMATHGoogle Scholar
  26. 26.
    Silva, M., Teruel, E., Colom, J.M.: Linear Algebraic and Linear Programming Techniques for the Analysis of Place/Transition Net Systems. In: Reisig, W., Rozenberg, G. (eds.) APN 1998. LNCS, vol. 1491, pp. 309–373. Springer, Heidelberg (1998)Google Scholar
  27. 27.
    Ullman, J.D.: Elements of ML Programming. Prentice-Hall, Englewood Cliffs (1998)Google Scholar
  28. 28.
    Valmari, A.: The State Explosion Problem. In Lectures on Petri Nets I: Basic Models. In: Reisig, W., Rozenberg, G. (eds.) APN 1998. LNCS, vol. 1491, pp. 429–528. Springer, Heidelberg (1998)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Lars Michael Kristensen
    • 1
  • Kurt Jensen
    • 1
  1. 1.Department of Computer ScienceUniversity of AarhusAarhus NDenmark

Personalised recommendations