Reasoning about Group-Based Mobility in MANETs

As one of the most interesting features of mobile ad hoc networks (MANETs), mobility may significantly affect the performance of network protocols. Realistic mobility models are not only decided by individual node movements, but also depend on node coordinations, such as group mobility. In this paper, we propose a process calculus for MANETs in which the motion path of a node is determined by both group mobility models and relative mobility models based on the reference point of the group it belongs to. Due to most of MANETs protocols are evaluated by simulation, a parametric framework is introduced to describe the mobility patterns, which can be used in the network simulation. Moreover, we develop an operational semantics to enable transitions in which the nodes may change their mobility patterns as computation proceeds or delay for some time, and we also give some semantic properties of our calculus based on these semantic rules. A weak bisimulation is provided to investigate the behavioral equivalence of the networks. Finally, a real-world case study about wireless hierarchical routing protocol with group mobility (WHIRL) is given to illustrate the applicability of our calculus.