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:arXiv.org 2015-12
Main Authors: Rob van Glabbeek, Höfner, Peter, Portmann, Marius, Wee Lum Tan
Format: Article
Language:English
Subjects:
Finite element method
Formal specifications
Mobile ad hoc networks
Modelling
Protocol
Protocol (computers)
Wireless networks
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:2331-8422
DOI:10.48550/arxiv.1512.08867