Modelling and verifying the AODV routing protocol

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 mo...

Full description

Saved in:
Bibliographic Details
Published in:Distributed computing 2016-08, Vol.29 (4), p.279-315
Main Authors: van Glabbeek, Rob, Höfner, Peter, Portmann, Marius, Tan, Wee Lum
Format: Article
Language:English
Subjects:
Algebra
Computer Communication Networks
Computer Hardware
Computer networks
Computer Science
Computer Systems Organization and Communication Networks
Maintenance
Mathematical analysis
Modelling
Routing (telecommunications)
Software Engineering/Programming and Operating Systems
Theory of Computation
Vectors (mathematics)
Wireless communication
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:0178-2770
1432-0452
DOI:10.1007/s00446-015-0262-7