• DocumentCode
    2949350
  • Title

    The proof of AODV loop freedom

  • Author

    Zhou, Ming ; Yang, Huabing ; Zhang, Xingyuan ; Wang, Jinshuang

  • Author_Institution
    Wuhan Univ. of Technol., Wuhan, China
  • fYear
    2009
  • fDate
    13-15 Nov. 2009
  • Firstpage
    1
  • Lastpage
    5
  • 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;
  • fLanguage
    English
  • Publisher
    ieee
  • 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
  • Type

    conf

  • DOI
    10.1109/WCSP.2009.5371479
  • Filename
    5371479
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=2949350