Process Calculi For Mobile AD Hoc Networks From A Group Perspective

Mobile Ad hoc Networks (MANETs) are networks dynamically formed by mobile nodes (PDAs, sensors, etc.) without the support of prior stationary infrastructures. In such a network, every node serves as a router or relay station to forward data to the destination node. Applications for MANETs in recent years are increasingly popular, ranging from distributed mobile computing to ambient intelligence, disaster recovery and military operations.In this paper we first present a probabilistic calculus for formally modeling and rea-soning about MANETs with unreliable connections and mobility of nodes. In our cal-culus, a MANET node can locally broadcast messages to a group of nodes within its physical transmission range. The group probability is also introduced since two distinct nodes within different groups should receive messages from the same sender with differ-ent possibilities. Our calculus naturally captures essential features of MANETs, i.e., local broadcast, mobility and probability. Moreover, we give a formal operational semantics of the calculus in terms of the labeled transition system. Moreover, we define the notion of open bisimulation and prove it to be a congruence relation. Based on this, we discuss sev-eral nontrivial properties of MANETs such as mobile node equivalence and replacement. Finally, we by a case study illustrate our calculus and use it to analyze the probability of a transmission via routines.Mobility is one of the inherent features of MANETs, and also one of the factors that most significantly affect the performance of network protocols. In this paper we also pro-pose a process calculus framework for MANETs, focusing on the group mobility. Group mobility models represent the random motion of a group of mobile nodes as well as the random motion of each individual mobile node within the group, we follow the para-metric framework presented by Godskesen and extend it for modeling mobility functions at two levels:the individual mobility model and the group mobility model. Moreover, we use a parameterized operational semantics to define the formal transitional rules for our calculus. Also we investigate behavioral equivalences of networks and provide a weak bisimulatin for our calculus. Finally, we show some non-trivial properties about MANETs and verify them in our calculus.