Abstract
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.
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 finite-control ω-processes. We also prove that the ω-calculus is a conservative extension of the π-calculus, and that late bisimulation (appropriately lifted from the π-calculus to the ω-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: τ-actions, as in the π-calculus, and μ-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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Basu, S., Ramakrishnan, C.R.: Compositional analysis for verification of parameterized systems. In: Garavel, H., Hatcliff, J. (eds.) ETAPS 2003 and TACAS 2003. LNCS, vol. 2619, pp. 315–330. Springer, Heidelberg (2003)
Cardelli, L., Gordon, A.D.: Mobile ambients. In: Nivat, M. (ed.) ETAPS 1998 and FOSSACS 1998. LNCS, vol. 1378, Springer, Heidelberg (1998)
Dam, M.: On the decidability of process equivalences for the π-calculus. Theoretical Computer Science 183, 215–228 (1997)
Ene, C., Muntean, T.: A broadcast-based calculus for communicating systems. In: Intl. Workshop on Formal Methods for Parallel Programming: Theory and Applications (2001)
Godskesen, J.C.: A calculus for mobile ad hoc networks. In: Murphy, A.L., Vitek, J. (eds.) COORDINATION 2007. LNCS, vol. 4467, pp. 132–150. Springer, Heidelberg (2007)
Godskesen, J.C., Gryn, O.: Modelling and verification of security protocols for ad hoc networks using UPPAAL. In: Proc. 18th Nordic Workshop on Programming Theory (October 2006)
Hennessy, M., Riely, J.: Resource access control in systems of mobile agents. In: High-Level Concurrent Languages. Electr. Notes Theor. Comput. Sci., vol. 16.3, pp. 3–17 (1998)
Merro, M.: An observational theory for mobile ad hoc networks. In: Proc. MFPS 2007. Electr. Notes Theor. Comput. Sci., vol. 173, pp. 275–293. Elsevier, Amsterdam (2007)
Mezzetti, N., Sangiorgi, D.: Towards a calculus for wireless systems. In: Proc. MFPS 2006. Electr. Notes Theor. Comput. Sci., vol. 158, pp. 331–354. Elsevier, Amsterdam (2006)
Milner, R.: The polyadic pi-calculus: a tutorial. In: Logic and Algebra of Specification, pp. 203–246. Springer, Heidelberg (1993)
Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, Parts I and II. Information and Computation 100(1), 1–77 (1992)
Nanz, S., Hankin, C.: A framework for security analysis of mobile wireless networks. Theoretical Computer Science 367(1-2), 203–227 (2006)
Ostrovsky, K., Prasad, K.V.S., Taha, W.: Towards a primitive higher order calculus of broadcasting systems. In: PPDP, pp. 2–13. ACM, New York (2002)
Prasad, K.V.S.: A calculus of broadcasting systems. Sci. Comput. Program. 25(2-3), 285–327 (1995)
Ramakrishna, Y.S., Ramakrishnan, C.R., Ramakrishnan, I.V., Smolka, S.A., Swift, T., Warren, D.S.: Efficient model checking using tabled resolution. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 143–154. Springer, Heidelberg (1997)
Singh, A., Ramakrishnan, C.R., Smolka, S.A.: A process calculus for mobile ad hoc networks (2008), http://www.lmc.cs.sunysb.edu/~anusingh/omega/
Vasudevan, S., Kurose, J.F., Towsley, D.F.: Design and analysis of a leader election algorithm for mobile ad hoc networks. In: ICNP, pp. 350–360. IEEE Computer Society, Los Alamitos (2004)
XSB. The XSB logic programming system, http://xsb.sourceforge.net
Yang, P., Basu, S., Ramakrishnan, C.R.: Parameterized verification of pi-calculus systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol. 3920, pp. 42–57. Springer, Heidelberg (2006)
Yang, P., Dong, Y., Ramakrishnan, C.R., Smolka, S.A.: A provably correct compiler for efficient model checking of mobile processes. In: Hermenegildo, M.V., Cabeza, D. (eds.) PADL 2004. LNCS, vol. 3350, pp. 113–127. Springer, Heidelberg (2005)
Yang, P., Ramakrishnan, C.R., Smolka, S.A.: A logical encoding of the pi-calculus: Model checking mobile processes using tabled resolution. International Journal on Software Tools for Technology Transfer (STTT) 6(1), 38–66 (2004)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Singh, A., Ramakrishnan, C.R., Smolka, S.A. (2008). A Process Calculus for Mobile Ad Hoc Networks. In: Lea, D., Zavattaro, G. (eds) Coordination Models and Languages. COORDINATION 2008. Lecture Notes in Computer Science, vol 5052. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-68265-3_19
Download citation
DOI: https://doi.org/10.1007/978-3-540-68265-3_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-68264-6
Online ISBN: 978-3-540-68265-3
eBook Packages: Computer ScienceComputer Science (R0)