Formal Verification of Route Request Procedure for AODV Routing Protocol

Main Article Content

Shakeel Ahmed
Nazir Ahmad Zafar


Many protocols have been designed for routing the packets from a source to destination. In Ad hoc on-demand routing protocol
(AODV) the routing table maintains only one route to the specified node. The route is rediscovered by the source node when the earlier route
fails. This paper aims to study the characteristics of Ad hoc networks and employ formal methods to model, investigate and analyze the routing
protocol. The Z notation is used as a formal technique because of its abstract properties. In the proposed approach, it is specified how a source
node can request for a route to the destination in AODV routing protocol. It is investigated how formal methods can be applied to the route
discovery process in the AODV routing protocol. Finally, the formal specification is analyzed and validated using Z Eves tool.




Keywords: AODV, Formal methods, Z notation, Route request procedure, verification.


Download data is not yet available.

Article Details