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 (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, which abstracts away from two types of internal actions: tau-actions, as in the pi-calculus, and mu-actions, signaling node movement. Finally, we illustrate the practical utility of the calculus by developing and analyzing a formal model of a leader-election protocol for MANETs.
Bibtex Entry:
@inproceedings{SRS:COORD08, author = {Anu Singh and C. R. Ramakrishnan and Scott A. Smolka}, title = {A Process Calculus for Mobile Ad Hoc Networks}, booktitle = {10th International Conference on Coordination Models and Languages (COORDINATION)}, address = {Oslo, Norway}, month = {June}, series = {Lecture Notes in Computer Science}, volume = {5052}, pages = {296--314}, publisher = {Springer}, year = {2008} }
| Full Paper: | [pdf] |
C. R. Ramakrishnan
(cram@cs.sunysb.edu)