Modeling and Efficient Verification of Wireless Ad hoc Networks

TL;DR

This paper introduces an actor-based modeling language for wireless ad hoc networks, enabling efficient verification of protocols like flooding and AODVv2-11 by abstracting key network behaviors and reducing state space complexity.

Contribution

It presents a novel modeling framework that captures topology dynamics and communication features of MANETs, facilitating formal verification of their protocols.

Findings

Effective modeling of topology changes and broadcast mechanisms

Significant reduction in state space for protocol verification

Detection of loop formation in AODV protocol

Abstract

Wireless ad hoc networks, in particular mobile ad hoc networks (MANETs), are growing very fast as they make communication easier and more available. However, their protocols tend to be difficult to design due to topology dependent behavior of wireless communication, and their distributed and adaptive operations to topology dynamism. Therefore, it is desirable to have them modeled and verified using formal methods. In this paper, we present an actor-based modeling language with the aim to model MANETs. We address main challenges of modeling wireless ad hoc networks such as local broadcast, underlying topology, and its changes, and discuss how they can be efficiently modeled at the semantic level to make their verification amenable. The new framework abstracts the data link layer services by providing asynchronous (local) broadcast and unicast communication, while message delivery is in order and is guaranteed for connected receivers. We illustrate the applicability of our framework through two routing protocols, namely flooding and AODVv2-11, and show how efficiently their state spaces can be reduced by the proposed techniques. Furthermore, we demonstrate a loop formation scenario in AODV, found by our analysis tool.