Abstract:
We present the omega-calculus, a process calculus for formally modeling and reasoning about Mobile Ad Hoc Wireless Networks (MANETs) and their protocols. The omega-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 omega-calculus is the separation of a node's communication and computational behavior, described by an omega-process, from the description of its physical transmission range, referred to as an omega-process interface.Our main technical results are as follows. We give a formal operational semantics of the omega-calculus in terms of labeled transition systems and show that the state reachability problem is decidable for finite-control omega-processes. We also prove that the omega-calculus is a conservative extension of the pi-calculus, and that late bisimulation equivalence (appropriately lifted from the pi-calculus to the omega-calculus) is a congruence. Congruence results are also established for a weak version of late bisimulation equivalence, which abstracts away from two types of internal actions: tau-actions, as in the pi-calculus, and mu-actions, signaling node movement. We additionally define a symbolic semantics for the omega-calculus extended with the mismatch operator, along with a corresponding notion of symbolic bisimulation equivalence, and establish congruence results for this extension as well. Finally, we illustrate the practical utility of the calculus by developing and analyzing formal models of a leader-election protocol for MANETs and the AODV routing protocol.
Bibtex Entry:
@article{SRS:SCP10, author = {Anu Singh and C. R. Ramakrishnan and Scott A. Smolka}, title = {A Process Calculus for Mobile Ad Hoc Networks}, journal = {Science of Computer Programming}, volume = {75}, number = {6}, pages = {440--469}, year = {2010} }
| Full Paper: | [pdf] |
C. R. Ramakrishnan
(cram@cs.sunysb.edu)