A Timed Process Algebra for Wireless Networks

TL;DR

This paper introduces a timed process algebra tailored for wireless networks, enabling detailed modeling and analysis of protocols like AODV, revealing loop issues and proposing fixes to improve protocol correctness.

Contribution

It extends the Algebra for Wireless Networks with timing features, allowing formal analysis of protocol properties such as loop freedom.

Findings

AODV protocol is not loop free under certain conditions

Boundary conditions can fix loop issues in AODV

The algebra facilitates protocol analysis and verification

Abstract

This paper proposes a timed process algebra for wireless networks, an extension of the Algebra for Wireless Networks. It combines treatments of local broadcast, conditional unicast and data structures, which are essential features for the modelling of network protocols. In this framework we model and analyse the Ad hoc On-Demand Distance Vector routing protocol, and show that, contrary to claims in the literature, it fails to be loop free. We also present boundary conditions for a fix ensuring that the resulting protocol is indeed loop free.