Modelling and verifying the AODV routing protocol

van Glabbeek, Rob, Hofner, Peter, Portmann, Marius and Tan, Wee Lum (2016) Modelling and verifying the AODV routing protocol. Distributed Computing, 29 4: 279-315. doi:10.1007/s00446-015-0262-7

Author van Glabbeek, Rob
Hofner, Peter
Portmann, Marius
Tan, Wee Lum
Title Modelling and verifying the AODV routing protocol
Journal name Distributed Computing   Check publisher's open access policy
ISSN 0178-2770
Publication date 2016-03-04
Year available 2016
Sub-type Article (original research)
DOI 10.1007/s00446-015-0262-7
Open Access Status Not Open Access
Volume 29
Issue 4
Start page 279
End page 315
Total pages 37
Place of publication Heidelberg, Germany
Publisher Springer
Collection year 2017
Language eng
Abstract This paper presents a formal specification of the Ad hoc On-demand Distance Vector (AODV) routing protocol using AWN (Algebra for Wireless Networks), a recent process algebra which has been 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 properties by providing detailed proofs of loop freedom and route correctness.
Keyword AODV
Loop freedom
Mobile ad-hoc networks
Process algebra
Routing protocols
Wireless mesh networks
Q-Index Code C1
Q-Index Status Provisional Code
Institutional Status UQ

Document type: Journal Article
Sub-type: Article (original research)
Collections: HERDC Pre-Audit
School of Information Technology and Electrical Engineering Publications
Version Filter Type
Citation counts: TR Web of Science Citation Count  Cited 0 times in Thomson Reuters Web of Science Article
Scopus Citation Count Cited 1 times in Scopus Article | Citations
Google Scholar Search Google Scholar
Created: Tue, 22 Mar 2016, 00:25:48 EST by System User on behalf of Learning and Research Services (UQ Library)