Modelling and Verifying the AODV Routing Protocol

TL;DR

This paper provides a formal specification of the AODV routing protocol using AWN process algebra, enabling rigorous reasoning about its core functionalities and correctness properties.

Contribution

It introduces a detailed formal model of AODV in AWN, facilitating proofs of loop freedom and route correctness, which was not previously formalized.

Findings

Formal model of AODV in AWN successfully verified for loop freedom.

Proved route correctness within the formal framework.

Enhanced understanding of AODV's core mechanisms through formal analysis.

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.