Loop Freedom in AODVv2 - Formal Techniques for Distributed Objects, Components, and Systems Access content directly
Conference Papers Year : 2015

Loop Freedom in AODVv2

Kedar S. Namjoshi
  • Function : Author
  • PersonId : 1030897
Richard J. Trefler
  • Function : Author
  • PersonId : 1030898


The AODV protocol is used to establish routes in a mobile, ad-hoc network (MANET). The protocol must operate in an adversarial environment where network connections and nodes can be added or removed at any point. While the ability to establish routes is best-effort under these conditions, the protocol is required to ensure that no routing loops are ever formed. AODVv2 is currently under development at the IETF, we focus attention on version 04. We detail two scenarios that show how routing loops may form in AODVv2 routing tables. The second scenario demonstrates a problem with the route table update performed on a Broken route entry. Our solution to this problem has been incorporated by the protocol designers into AODVv2, version 05. With the fix in place, we present an inductive and compositional proof showing that the corrected core protocol is loop-free for all valid configurations.
Fichier principal
Vignette du fichier
978-3-319-19195-9_7_Chapter.pdf (297.15 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-01767329 , version 1 (16-04-2018)





Kedar S. Namjoshi, Richard J. Trefler. Loop Freedom in AODVv2. 35th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2015, Grenoble, France. pp.98-112, ⟨10.1007/978-3-319-19195-9_7⟩. ⟨hal-01767329⟩
86 View
99 Download



Gmail Facebook X LinkedIn More