Formal Descriptionof aDistributedLocationServic for e.pdf

Formal Description of aDistributed Location Servic e for Mobile Ad Hoc Networks András Benczúr1, Uwe Gl?sser2 and Tamás Lukovszki3 1Computer Science Research Institute of the Hungari an Academy of Sciences, benczur@sztaki.hu 2School of Computing Science, Simon Fraser Universi ty, BC, Canada, glaesser@cs.sfu.ca 3Heinz Nixdorf Institute, Paderborn University, Ger many, tamas@hni.upb.de Abstract. 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 ubstantially different fr om those used in static ommu- 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 ault-tolerance thereby improving sta te-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 routin g 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 oncepts, such as concurrency, reactivity and asynchronism, directly with the related concepts as imposed by the given application context. 1 Introduction In this paper, we define a distributed abstract state machine (DASM) model [7] of the network or routing layer protocol for mobile ad hoc network s. Such networks are de- signed for wireless communication and require no fixed infrastructure as the mobile hosts also perform routing tasks [13]. Thus, they a re particularly suitable, for instance, for escue opera