A Process Calculus for Mobile Ad Hoc Networks

We present the -calculus, a process calculus for formally modeling and reasoning about Mobile Ad Hoc Wireless Networks (MANETs) and their protocols. The -calculus naturally captures essential characteristics of MANETs, including the ability of a MANET node to broadcast a message to any other node within its physical transmission range (and no others), and to move in and out of the transmission range of other nodes in the network. A key feature of the -calculus is the separation of a node's communication and computational behavior, described by an -process, from the description of its physical transmission range, referred to as an -process interface. We demonstrate that, in comparison to the -calculus, attempts to model MANET behavior in existing process calculi prove cumbersome. Our main technical results are as follows. We give a formal operational semantics of the -calculus in terms of labeled transition systems and show that the state reachability problem is decidable for finit...

• Type: Conference
• Year: 2008
• Where: COORDINATION
• Authors: Anu Singh, C. R. Ramakrishnan, Scott A. Smolka
• Keywords: COORDINATION 2008, Distributed And Parallel Computing, MANET, MANET Node, Physical Transmission Range