Analysis and Validation of AODV Routing Protocol Using Timed Colored Petri Net

Abstract

Due to the nondeterministic nature of concurrent systems it is very challenging to design and develop the system. Nondeterministic systems can execute in more than one ways, so have a limitless number of probable executions. It increases the chance of any designer or modeller to miss certain imperative properties of such systems which prompts to a faulty and defective system. Therefore it is highly required to use methods before its actual deployment and implementation that can test and debug the primary system design. The most feasible way to handle the unavoidable and undetected errors or problems of constructing any concurrent system is to build a model of that system before its actual development. Among various modelling technique, Petri net model has been proved to be a best formal technique for modelling and validating distributed and concurrent systems [1].
One major application area of Petri nets is modelling routing protocols which ensures that it is unambiguous and functionality correct. Aa hoc On demand Routing Protocol(AODV) is one of the basic dynamic routing protocol, where nodes changes their postiotion contineously in the network. In this way it is especially important for each node in the system to monitor changes so that a productive packet transmission should be possible. In this thesis Timed CPN which is an extension of basic Petri nets, which is used to model and validate the working of AODV protocol in the concurrent environment. Petri nets have been effectively demonstrated the correctness of various communication protocols. AODV protocol is modelled in which an efficient packet transmission is done in the network with the node movement and frequent topology changes. The Timed CPN model aimed to detect and maintain the routes in the dynamic environment and validate the key properties of AODV protocol.