  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.
