Formal Modelling and Analysis of AODV

Wireless systems have a wide range of applications recently. To explore complex features of such systems, formalisms are proposed to specify and reason about them. This paper presents a case study of routing protocol in wireless networks. We formalize the route discovery process of AODV routing protocol using Object-Z. Network topology and local variables of nodes are defined by relations and functions. The broadcast communication is modelled by operations which change local variables of the sender and all of its connected receivers simultaneously. We show the proof of loop freedom property for established routes based on the specification. Further, the specification is modified by adding mobility of nodes and loop freedom under a dynamic network topology is discussed, showing the scalability of our approach.