A rigorous analysis of AODV and its variants

Hoefner, Peter, van Glabbeek, Robert J., Tan, Wee Lum, Portmann, Marius, McIver, Annabelle and Fehnker, Ansgar (2012). A rigorous analysis of AODV and its variants. In: MSWiM '12: Proceedings of the 15th ACM International Conference on Modeling, Analysis and Simulation of Wireless and Mobile Systems. 15th ACM International Conference on Modeling, Analysis and Simulation of Wireless and Mobile Systems (MSWiM '12), Paphos, Cyprus, (203-212). 21-25 October 2012. doi:10.1145/2387238.2387274

Attached Files (Some files may be inaccessible until you login with your UQ eSpace credentials)
Name Description MIMEType Size Downloads

Author Hoefner, Peter
van Glabbeek, Robert J.
Tan, Wee Lum
Portmann, Marius
McIver, Annabelle
Fehnker, Ansgar
Title of paper A rigorous analysis of AODV and its variants
Conference name 15th ACM International Conference on Modeling, Analysis and Simulation of Wireless and Mobile Systems (MSWiM '12)
Conference location Paphos, Cyprus
Conference dates 21-25 October 2012
Proceedings title MSWiM '12: Proceedings of the 15th ACM International Conference on Modeling, Analysis and Simulation of Wireless and Mobile Systems
Journal name MSWiM'12 - Proceedings of the 15th ACM International Conference on Modeling, Analysis and Simulation of Wireless and Mobile Systems
Place of Publication New York, United States
Publisher ACM
Publication Year 2012
Sub-type Fully published paper
DOI 10.1145/2387238.2387274
Open Access Status
ISBN 9781450316286
Start page 203
End page 212
Total pages 10
Collection year 2013
Language eng
Abstract/Summary In this paper we present a rigorous analysis of the Ad hoc On-Demand Distance Vector (AODV) routing protocol using a formal specification in AWN (Algebra for Wireless Networks), a process algebra which has been specifically tailored for the modelling of Mobile Ad Hoc Networks and Wireless Mesh Network protocols. Our formalisation models the exact details of the core functionality of AODV, such as route discovery, route maintenance and error handling. We demonstrate how AWN can be used to reason about critical protocol correctness properties by providing a detailed proof of loop freedom. In contrast to evaluations using simulation or other formal methods such as model checking, our proof is generic and holds for any possible network scenario in terms of network topology, node mobility, traffic pattern, etc. A key contribution of this paper is the demonstration of how the reasoning and proofs can relatively easily be adapted to protocol variants.
Keyword AODV
Loop freedom
Process algebra
Routing protocols
Wireless mesh networks
Q-Index Code E1
Q-Index Status Confirmed Code
Institutional Status UQ

 
Versions
Version Filter Type
Citation counts: Scopus Citation Count Cited 8 times in Scopus Article | Citations
Google Scholar Search Google Scholar
Created: Wed, 03 Apr 2013, 16:59:29 EST by Dr Marius Portmann on behalf of School of Information Technol and Elec Engineering