Formal description and analysis of a distributed location service for mobile ad hoc networks

In this paper, we define a distributed abstract state machine (DASM) model of the network or routing layer protocol for mobile ad hoc networks. In conjunction with the chosen routing strategy, we propose a distributed logical topology based location service (LTLS) protocol and give a formal description and analysis of this protocol on the DASM model. The high dynamics of mobile ad hoc networks require routing strategies substantially different from those used in static communication networks. A strategy for such networks is geographic routing in which each network node can find its physical location via GPS or other navigation technologies. To send a packet, the sender needs to know the most recent physical location of the destination node. This location information is provided by a location service protocol. The LTLS protocol has short message delivery delay, requires small routing tables, uses relatively few administrative packets, and has very good fault tolerance properties. Our goal in defining the network layer protocol in terms of a DASM model is twofold. First, we feel that the mathematical modeling paradigm of distributed abstract state machines provides an ideal formal basis for constructing, analyzing, and validating abstract requirements specifications of mobile ad hoc network protocols. Second, we intend to utilize the resulting behavior model as a formal basis for developing executable specifications serving as a platform for experimental validation of key system attributes and exploration of alternative design choices.