Formal Methods for Mobile Ad Hoc Networks: A Survey

TL;DR

This survey reviews formal methods used to analyze the correctness, performance, and security of mobile ad hoc network protocols, highlighting frameworks, models, and applications specific to MANETs.

Contribution

It provides a comprehensive overview of formal analysis techniques and frameworks tailored for MANET routing protocols, consolidating scattered research in this field.

Findings

Formal methods improve protocol correctness verification

Analysis techniques cover security and real-time properties

Overview of mobility models and formal frameworks

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.