TY - GEN
T1 - Reasoning about group-based mobility in MANETs
AU - Wu, Xi
AU - Liu, Si
AU - Zhu, Huibiao
AU - Zhao, Yongxin
N1 - Publisher Copyright:
© 2014 IEEE.
PY - 2014/12/3
Y1 - 2014/12/3
N2 - 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.
AB - 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.
UR - https://www.scopus.com/pages/publications/84919466249
U2 - 10.1109/PRDC.2014.39
DO - 10.1109/PRDC.2014.39
M3 - 会议稿件
AN - SCOPUS:84919466249
T3 - Proceedings of IEEE Pacific Rim International Symposium on Dependable Computing, PRDC
SP - 244
EP - 253
BT - Proceedings - 20th IEEE Pacific Rim International Symposium on Dependable Computing, PRDC 2014
PB - IEEE Computer Society
T2 - 20th IEEE Pacific Rim International Symposium on Dependable Computing, PRDC 2014
Y2 - 19 November 2014 through 21 November 2014
ER -