Formal Description of a Distributed Location Service for Mobile Ad Hoc Networks

We define here a distributed abstract state machine (DASM) [7] of the network or routing layer of mobile ad hoc networks [13]. Such networks re- quire routing strategies substantially different from those used in static commu- nication networks, since storing and updating large routing tables at mobile hosts would congest the network with administration packets very fast. In [1], the hypercubic location service is presented, which considers a very strong definition of fault-tolerance thereby improving state-of-the-art ad hoc routing protocols in several respects. Our goal in modeling the protocols for the distrib- uted location service and the position based routing is twofold. First, we support the definition and validation of wireless communication protocols and imple- mentations based thereon. Second, we feel that the abstract computation model naturally reflects the layering principle of communication architectures in com- bination with an uncompromisingly local view of the application domain. Thus we can identify fundamental semantic concepts, such as concurrency, reactivity and asynchronism, directly with the related concepts as imposed by the given application context.