Formal modeling of traffic based flooding procedure of AODV for Mobile Ad hoc Networks

Rapid advancement in ad hoc networks and its variants, create a need for efficient and accurate routing decisions. As routing decisions for Mobile Ad hoc Networks has great impact on the overall performance of the network Quality of Service (QoS) parameters (delay, bandwidth, PDR etc.), optimized routing protocols need to be designed. One of the biggest challenges in designing ad hoc routing protocols is to attain the bounded delay and finding the best path/route to the desired node. Ad hoc ondemand Distance Vector (AODV) routing protocol has a single path to the specified node in its routing table without considering various parameters. In this paper, traffic based flooding procedure for AODV protocol is proposed and defined by using formal methods. The procedure states that the data packets generated in the network will first be categorized according to their packet type and then a specific data rate will be assigned for that packet to avoid the redundant overhead on the links. The complete model is designed by using formal methods because formal methods are the most emerging techniques based on mathematics. VDM-SL (formal language/notation) is used to specify the complete and detailed level proposed models' specifications. The procedure is then verified and validated through VDM-SL toolbox.