2011 IEEE 13th International Symposium on High-Assurance Systems Engineering (2011)
Boca Raton, Florida USA
Nov. 10, 2011 to Nov. 12, 2011
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/HASE.2011.13
Mobile Ad hoc Networks (MANETs) are networks dynamically formed by mobile nodes without the support of prior stationary infrastructures. The essential features of such a network are local broadcast, mobility and probability. In our earlier work, we proposed the pw-calculus to formally model and reason about MANTEs from a group probabilistic perspective, in which a MANET node can locally broadcast messages to a group of nodes within its physical transmission range with a certain probability. The group probabilities depend on the network topology which can evolve with the mobility of nodes. In this paper, to capture the behavior equivalence of networks, the structural congruence is investigated and the operational semantics is refined. Moreover, we define the notion of open bisimulation and prove it to be a congruence relation. Based on this, we discuss several 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.
Mobile Ad Hoc Networks, Formal Modeling, Operational Semantics, Open Bisimulation, Probability
H. Zhu, Q. Li, S. Liu and Y. Zhao, "A Calculus for Mobile Ad Hoc Networks from a Group Probabilistic Perspective," 2011 IEEE 13th International Symposium on High-Assurance Systems Engineering(HASE), Boca Raton, Florida USA, 2011, pp. 157-162.