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.

翻译：在移动自组织网络（MANET）中，通信采用无线方式且节点可独立移动。正确分析MANET协议的功能正确性、性能与安全性是一项具有挑战性的任务。目前已有多种形式化规约与分析技术被应用于MANET协议的分析。本综述系统梳理了严格的形式化分析技术及其应用，重点关注MANET路由协议。除功能正确性外，亦考量实时特性与安全属性。此外，本文概述了专门针对MANET设计的形化框架，以及作为MANET协议性能分析基础的移动性模型。旨在为这一相对分散的研究领域提供全面而连贯的综述，该领域已运用多种严格的形式化方法来分析各类MANET协议的不同层面。