Abstract
We propose a process algebra for wireless mesh networks that combines novel treatments of local broadcast, conditional unicast and data structures. In this framework, we model the Ad-hoc On-Demand Distance Vector (AODV) routing protocol and (dis)prove crucial properties such as loop freedom and packet delivery.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Kernel AODV (v. 2.2.2), NIST, http://www.antd.nist.gov/wctg/aodv_kernel/ (accessed January 6, 2012)
AODV-UU: An implementation of the AODV routing protocol (IETF RFC 3561), http://sourceforge.net/projects/aodvuu/ (accessed January 6, 2012)
Bhargavan, K., Obradovic, D., Gunter, C.A.: Formal verification of standards for distance vector routing protocols. J. ACM 49(4), 538–576 (2002), http://dx.doi.org/10.1145/581771.581775
Cleaveland, R., Lüttgen, G., Natarajan, V.: Priority in process alegbra. In: Handbook of Process Algebra, ch.12, pp. 711–765. Elsevier (2001)
Cranen, S., Mousavi, M.R., Reniers, M.A.: A Rule Format for Associativity. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 447–461. Springer, Heidelberg (2008)
Fehnker, A., van Glabbeek, R.J., Höfner, P., McIver, A., Portmann, M., Tan, W.L.: A process algebra for wireless mesh networks used for modelling, verifying and analysing AODV. Tech. Rep. 5513, NICTA (2012), http://www.nicta.com.au/pub?id=5513
Ghassemi, F., Fokkink, W.J., Movaghar, A.: Restricted broadcast process theory. In: Proc. IEEE SEFM 2008 (2008)
Godskesen, J.C.: A Calculus for Mobile Ad Hoc Networks. In: Murphy, A.L., Ryan, M. (eds.) COORDINATION 2007. LNCS, vol. 4467, pp. 132–150. Springer, Heidelberg (2007)
Groote, J.F., Ponse, A.: The syntax and semantics of μCRL. In: Algebra of Communicating Processes 1994. Workshops in Computing, pp. 26–62. Springer, Heidelberg (1995)
Hiertz, G.R., Denteneer, D., Max, S., Taori, R., Cardona, J., Berlemann, L., Walke, B.: IEEE 802.11s: the WLAN mesh standard. IEEE Wireless Communications 17(1), 104–111 (2010), http://dx.doi.org/10.1109/MWC.2010.5416357
Lynch, N., Tuttle, M.: An introduction to input/output automata. CWI-Quarterly 2(3), 219–246 (1989); centrum voor Wiskunde en Informatica, Amsterdam, The Netherlands
Merro, M.: An observational theory for mobile ad hoc networks. Inf. Comput. 207(2), 194–208 (2009)
Mezzetti, N., Sangiorgi, D.: Towards a calculus for wireless systems. Electr. Notes Theor. Comput. Sci. 158, 331–353 (2006)
Miskovic, S., Knightly, E.W.: Routing primitives for wireless mesh networks: Design, analysis and experiments. In: IEEE INFOCOM, pp. 2793–2801 (2010), http://dx.doi.org/10.1109/INFCOM.2010.5462111
Nanz, S., Hankin, C.: A framework for security analysis of mobile wireless networks. Theor. Comput. Sci. 367, 203–227 (2006)
Perkins, C., Belding-Royer, E., Das, S.: Ad hoc on-demand distance vector (AODV) routing. RFC 3561 (2003), http://www.ietf.org/rfc/rfc3561.txt
Plotkin, G.: A structural approach to operational semantics. The Journal of Logic and Algebraic Programming 60- 61, 17–139 (2004) (originally appeared in 1981)
Prasad, K.V.S.: A calculus of broadcasting systems. Sci. Comput. Program. 25(2-3), 285–327 (1995)
de Simone, R.: Higher-level synchronising devices in Meije-SCCS. Theor. Comput. Sci. 37, 245–267 (1985)
Singh, A., Ramakrishnan, C.R., Smolka, S.A.: A process calculus for mobile ad hoc networks. Science of Computer Programming 75, 440–469 (2010)
Zhou, M., Yang, H., Zhang, X., Wang, J.: The proof of AODV loop freedom. In: Proc. IEEE WCSP (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fehnker, A., van Glabbeek, R., Höfner, P., McIver, A., Portmann, M., Tan, W.L. (2012). A Process Algebra for Wireless Mesh Networks. In: Seidl, H. (eds) Programming Languages and Systems. ESOP 2012. Lecture Notes in Computer Science, vol 7211. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28869-2_15
Download citation
DOI: https://doi.org/10.1007/978-3-642-28869-2_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-28868-5
Online ISBN: 978-3-642-28869-2
eBook Packages: Computer ScienceComputer Science (R0)