A Process Algebra for Wireless Mesh Networks

TL;DR

This paper introduces a process algebra tailored for wireless mesh networks, enabling formal modeling and verification of protocols like AODV, including properties like loop freedom and packet delivery.

Contribution

It presents a novel process algebra framework that captures key wireless network features and applies it to model and verify the AODV routing protocol.

Findings

Model successfully verifies loop freedom.

Model confirms packet delivery properties.

Framework handles local broadcast and unicast effectively.

Abstract

We propose a process algebra for wireless mesh networks that combines novel treatments of local broadcast, conditional unicast and data structures. In this framework, we model the Ad-hoc On-Demand Distance Vector (AODV) routing protocol and (dis)prove crucial properties such as loop freedom and packet delivery.