Validation of Ad hoc On-Demand Multipath Distance Vector Using Colored Petri Nets

For a successful application of MANETS, it is very important to ensure that a routing protocol is unambiguous, complete and functionally correct. One approach to ensuring correctness of an existing routing protocol is to create a formal model for the protocol, and analyze the model to determine if needed the protocol provides the defined service correctly. Colored Petri Nets (CPNs) are a suitable modeling language for this purpose. However it is not easy to build a CPN model of a MANET because a node can move in and out of its transmission range and thus the MANET' topology dynamically changes.