VERIFYING ROUTE REQUEST PROCEDURE OF AODV USING GRAPH THEORY AND FORMAL METHODS

Phenomenal growth both in wireless ad hoc networks and network-based real time applications has led torapid change in the industry. For this purpose various protocols are designed for routing packets fromsource to destination to attain a better Quality of Service (QoS), which requires a mechanism thatguarantees bounded delay and jitter. Finding the best route to destination satisfying the QoS for real-timeinteractive application has become a challenge for today’s network services. The routing table of Ad hocon-demand routing protocol (AODV) maintains only one route to the specified node without consideringthe other important parameters. This paper proposes a Formal framework to improve the QoS bysearching the graph using formal techniques. The searching technique is based on considering packet typeand battery life. Because the nodes of AODV protocol are not fixed hence the dynamic graphs are used tomodel the network topology. The Z notation is used to transform the graph into formal specification of theprotocol. Finally, the formal specification is analyzed and validated using Z Eves tool.