Title :
The proof of AODV loop freedom
Author :
Zhou, Ming ; Yang, Huabing ; Zhang, Xingyuan ; Wang, Jinshuang
Author_Institution :
Wuhan Univ. of Technol., Wuhan, China
Abstract :
Loop freedom is an important property for distance vector routing protocols, especially for the protocols of ad hoc network because the topologies are dynamic. This paper gives a formal description of the AODV protocol and presents a strictly formal proof of its loop freedom property in Isabelle/HOL. The proved theorem states that no loop will exist in any number of nodes. The result demonstrates the feasibility of completely formal verification of some properties of routing protocols with reasonable effort.
Keywords :
ad hoc networks; formal verification; routing protocols; AODV protocol; Isabelle/HOL; ad hoc network; distance vector routing protocols; formal verification; loop freedom; Ad hoc networks; Computer bugs; Formal verification; Mobile ad hoc networks; Network topology; Programmable logic arrays; Radar; Routing protocols; Testing; Unicast; AODV; Isabelle; Loop Freedom; Routing Protocol;
Conference_Titel :
Wireless Communications & Signal Processing, 2009. WCSP 2009. International Conference on
Conference_Location :
Nanjing
Print_ISBN :
978-1-4244-4856-2
Electronic_ISBN :
978-1-4244-5668-0
DOI :
10.1109/WCSP.2009.5371479
