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.