Formal Methods for Mobile Ad Hoc Networks: A Survey

TL;DR

This survey addresses the challenge of verifying MANET routing protocols under dynamic mobility, timing, and security constraints by surveying rigorous formal methods. It maps a spectrum of approaches—from model checking and interactive theorem proving to specialized process calculi and mobility-aware frameworks—to analyzes of routing protocols like AODV and OLSR, including real-time and security properties. Key contributions include a consolidation of frameworks tailored to MANETs (notably AWN and related calculi), insights into broadcast semantics and topology-aware reasoning, and guidance on when to use model checking, process calculi, or theorem proving. The work highlights successful flaw detection and protocol refinements enabled by formal analyses, and it advocates a hybrid, practitioner-friendly verification pipeline to facilitate broader adoption in protocol development and certification.

Abstract

In a mobile ad hoc network (MANET), communication is wireless and nodes can move independently. Properly analyzing the functional correctness, performance, and security of MANET protocols is a challenging task. A wide range of formal specification and analysis techniques have been employed in the analysis of MANET protocols. This survey presents an overview of rigorous formal analysis techniques and their applications, with a focus on MANET routing protocols. Next to functional correctness, also real-time properties and security are considered. Moreover, an overview is given of formal frameworks that target MANETs specifically, as well as mobility models that underlie performance analyses of MANET protocols. The aim is to give a comprehensive and coherent overview of this rather scattered field, in which a variety of rigorous formal methods have been applied to analyze different aspects of a wide range of MANET protocols.