Abstract
This paper presents a formal specification of the Ad hoc On-demand Distance Vector (AODV) routing protocol using AWN (Algebra for Wireless Networks), a recent process algebra which has been tailored for the modelling of mobile ad hoc networks and wireless mesh network protocols. Our formalisation models the exact details of the core functionality of AODV, such as route discovery, route maintenance and error handling. We demonstrate how AWN can be used to reason about critical protocol properties by providing detailed proofs of loop freedom and route correctness.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Bergstra J.A., Klop J.W.: Algebra of communicating processes with abstraction. Theor. Comput. Sci. 37(1), 77–121 (1985)
Bhargavan K., Gunter C.A., Kim M., Lee I., Obradovic D., Sokolsky O., Viswanathan M.: Verisim: formal analysis of network simulations. IEEE Trans. Softw. Eng. 28(2), 129–145 (2002). doi:10.1109/32.988495
Bhargavan K., Obradovic D., Gunter C.A.: Formal verification of standards for distance vector routing protocols. JACM 49(4), 538–576 (2002). doi:10.1145/581771.581775
Bolognesi T., Brinksma E.: Introduction to the ISO specification language LOTOS. Comput. Netw. 14, 25–59 (1987). doi:10.1016/0169-7552(87)90085-7
Borgström, J., Huang, S., Johansson, M., Raabjerg, P., Victor, B., Pohjola, J.Å., Parrow, J.: Broadcast psi-calculi with an application to wireless protocols. In: Barthe, G., Pardo, A., Schneider, G. (eds.) Software Engineering and Formal Methods (SEFM’11), Lecture Notes in Computer Science, vol. 7041, pp. 74–89. Springer (2011). doi:10.1007/978-3-642-24690-6_7
Bourke, T., van Glabbeek, R.J., Höfner, P.: A mechanized proof of loop freedom of the (untimed) AODV routing protocol. In: Cassez, F., Raskin, J.F. (eds.) Automated Technology for Verification and Analysis (ATVA’14), Lecture Notes in Computer Science, vol. 8837, pp. 47–63. Springer (2014). doi:10.1007/978-3-319-11936-6_5
Bourke, T., van Glabbeek, R.J., Höfner, P.: Showing invariance compositionally for a process algebra for network protocols. In: Klein, G., Gamboa, R. (eds.) Interactive Theorem Proving (ITP’14), Lecture Notes in Computer Science, vol. 8558, pp. 144–159. Springer (2014). doi:10.1007/978-3-319-08970-6_10
Bres, E., van Glabbeek, R.J., Höfner, P.: A Timed Process Algebra for Wireless Networks with an Application in Routing. Technical Report 9145, NICTA (2016). http://nicta.com.au/pub?id=9145 [Extended Abstract in: Thiemann, P. (ed.) European Symposium on Programming (ESOP ’16). Lecture Notes in Computer Science, vol. 9632. Springer (2016). doi: 10.1007/978-3-662-49498-1_5]
Chiyangwa, S., Kwiatkowska, M.: A timing analysis of AODV. In: Formal Methods for Open Object-based Distributed Systems (FMOODS’05), Lecture Notes in Computer Science, vol. 3535, pp. 306–322. Springer (2005). doi:10.1007/11494881_20
Clausen, T., Jacquet, P.: Optimized link state routing protocol (OLSR). RFC 3626 (Experimental), Network Working Group (2003). http://www.ietf.org/rfc/rfc3626.txt
Das S.R., Castañeda R., Yan J.: Simulation-based performance evaluation of routing protocols for mobile ad hoc networks. Mob. Netw. Appl. 5(3), 179–189 (2000). doi:10.1023/A:1019108612308
Edenhofer, S., Höfner, P.: Towards a rigorous analysis of AODVv2 (DYMO). In: Rigorous Protocol Engineering (WRiPE ’12). IEEE (2012). doi:10.1109/ICNP.2012.6459942
Ene, C., Muntean, T.: A broadcast-based calculus for communicating systems. In: Parallel and Distributed Processing Symposium (IPDPS ’01), pp. 1516–1525. IEEE Computer Society (2001). doi:10.1109/IPDPS.2001.925136
Fehnker, A., van Glabbeek, R.J., Höfner, P., McIver, A.K., Portmann, M., Tan, W.L.: Automated analysis of AODV using UPPAAL. In: Flanagan, C., König, B. (eds.) Tools and Algorithms for the Construction and Analysis of Systems (TACAS ’12), Lecture Notes in Computer Science, vol. 7214, pp. 173–187. Springer (2012). doi:10.1007/978-3-642-28756-5_13
Fehnker, A., van Glabbeek, R.J., Höfner, P., McIver, A.K., Portmann, M., Tan, W.L.: A process algebra for wireless mesh networks. In: Seidl, H. (ed.) European Symposium on Programming (ESOP ’12)x, Lecture Notes in Computer Science, vol. 7211, pp. 295–315. Springer (2012). doi:10.1007/978-3-642-28869-2_15
Fehnker, A., van Glabbeek, R.J., Höfner, P., McIver, A.K., Portmann, M., Tan, W.L.: A process algebra for wireless mesh networks used for modelling, verifying and analysing AODV. Technical Report 5513, NICTA (2013). http://arxiv.org/abs/1312.7645
Garcia-Luna-Aceves, J.J.: A unified approach to loop-free routing using distance vectors or link states. In: Symposium Proceedings on Communications, Architectures and Protocols (SIGCOMM ’89), ACM SIGCOMM Computer Communication Review, vol. 19(4), pp. 212–223. ACM Press (1989). doi:10.1145/75246.75268
Garcia-Luna-Aceves, J.J., Rangarajan, H.: A new framework for loop-free on-demand routing using destination sequence numbers. In: Mobile Ad-hoc and Sensor Systems (MASS’ 04), pp. 426–435. IEEE (2004). doi:10.1109/MAHSS.2004.1392182
Ghassemi, F., Fokkink, W., Movaghar, A.: Restricted broadcast process theory. In: Cerone, A., Gruner, S. (eds.) Software Engineering and Formal Methods (SEFM ’08), pp. 345–354. IEEE Computer Society (2008). doi:10.1109/SEFM.2008.25
Godskesen, J.C.: A calculus for mobile ad hoc networks. In: Murphy, A.L., Vitek, J. (eds.) Coordination Models and Languages (COORDINATION ’07), Lecture Notes in Computer Science, vol. 4467, pp. 132–150. Springer (2007). doi:10.1007/978-3-540-72794-1_8
Godskesen, J.C.: Observables for mobile and wireless broadcasting systems. In: Clarke, D., Agha, G.A. (eds.) Coordination Models and Languages (COORDINATION ’10), Lecture Notes in Computer Science, vol. 6116, pp. 1–15. Springer (2010). doi:10.1007/978-3-642-13414-2_1
Griffin T.G., Sobrinho J.: Metarouting. SIGCOMM Comput. Commun. Rev. 35(4), 1–12 (2005). doi:10.1145/1090191.1080094
Guerrero-Zapata, M., Asokan, N.: Securing Ad Hoc Routing Protocols. In: Proceedings of the 2002 ACM Workshop on Wireless Security (WiSe 2002), pp. 1–10. ACM Press (2002). doi:10.1145/570681.570682
Hoare C.A.R.: Communicating Sequential Processes. Prentice Hall, Englewood Cliffs (1985)
Höfner, P., van Glabbeek, R.J., Tan, W.L., Portmann, M., McIver, A.K., Fehnker, A.: A rigorous analysis of AODV and its variants. In: Modeling, Analysis and Simulation of Wireless and Mobile Systems (MSWiM ’12), pp. 203–212. ACM Press (2012). doi:10.1145/2387238.2387274
IEEE: IEEE Standard for Information Technology—Telecommunications and information exchange between systems—Local and metropolitan area networks—Specific requirements Part 11: Wireless LAN Medium Access Control (MAC) and Physical Layer (PHY) specifications Amendment 10: Mesh Networking (2011). http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=6018236
Jacquet, P., Laouiti, A., Minet, P., Viennot, L.: Performance of multipoint relaying in ad hoc mobile routing protocols. In: Gregori, E., Conti, M., Campbell, A.T., Omidyar, G., Zukerman, M. (eds.) Networking Technologies, Services, and Protocols; Performance of Computer and Communication Networks; Mobile and Wireless Communications (NETWORKING ’02), Lecture Notes in Computer Science, pp. 387–398. Springer (2002). doi:10.1007/3-540-47906-6_31
Johnson, D., Hu, Y., Maltz, D.: The dynamic source routing protocol (DSR) for mobile ad hoc networks for IPv4. RFC 4728 (Experimental), Network Working Group (Errata Exist) (2007). http://www.ietf.org/rfc/rfc4728.txt
Maltz D., Broch J., Johnson D.B.: Lessons from a full-scale multihop wireless ad hoc network testbed. IEEE Pers. Commun. 8(1), 8–15 (2001). doi:10.1109/98.904894
Merlin P.M., Segall A.: A failsafe distributed routing protocol. IEEE Trans. Commun. 27(9), 1280–1287 (1979). doi:10.1109/TCOM.1979.1094552
Merro M.: An observational theory for mobile ad hoc networks (full version). Inf. Comput. 207(2), 194–208 (2009). doi:10.1016/j.ic.2007.11.010
Mezzetti N., Sangiorgi D.: Towards a calculus for wireless systems. Electr. Notes Theor. Comput. Sci. 158, 331–353 (2006). doi:10.1016/j.entcs.2006.04.017
Milner R.: Communication and Concurrency. Prentice Hall, Englewood Cliffs (1989)
Miskovic, S., Knightly, E.W.: Routing primitives for wireless mesh networks: design, analysis and experiments. In: Conference on Information Communications (INFOCOM ’10), pp. 2793–2801. IEEE (2010). doi: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). doi:10.1016/j.tcs.2006.08.036
Neumann, A., Aichele C. Lindner, M., Wunderlich, S.: Better approach to mobile ad-hoc networking (B.A.T.M.A.N.). Internet-Draft (Experimental), Network Working Group (2008). http://tools.ietf.org/html/draft-openmesh-b-a-t-m-a-n-00
The network simulator ns-2. http://nsnam.isi.edu/nsnam/index.php/Main_Page (accessed 20 December 2013)
Perkins, C.E., Belding-Royer, E.M., Das, S.: Ad hoc on-demand distance vector (AODV) routing. RFC 3561 (Experimental), Network Working Group (2003). http://www.ietf.org/rfc/rfc3561.txt
Perkins C.E., Belding-Royer E.M., Das S.R., Marina M.K.: Performance comparison of two on-demand routing protocols for ad hoc networks. IEEE Pers. Commun. 8(1), 16–28 (2001). doi:10.1109/98.904895
Perkins, C.E., Ratliff, S., Dowdell, J.: Dynamic MANET on-demand (AODVv2) routing. Internet Draft (Standards Track), Mobile Ad hoc Networks Working Group (2013). http://tools.ietf.org/html/draft-ietf-manet-aodvv2-02
Perkins, C.E., Royer, E.M.: Ad-hoc on-demand distance vector routing. In: Mobile Computing Systems and Applications (WMCSA ’99), pp. 90–100. IEEE (1999). doi:10.1109/MCSA.1999.749281
Pirzada A.A., Portmann M., Indulska J.: Performance analysis of multi-radio AODV in hybrid wireless mesh networks. Comput. Commun. 31(5), 885–895 (2008). doi:10.1016/j.comcom.2007.12.012
Pirzada A.A., Portmann M., Wishart R., Indulska J.: SafeMesh: a wireless mesh network routing protocol for incident area communications. Pervas. Mobile Comput. 5(2), 201–221 (2009). doi:10.1016/j.pmcj.2008.11.005
Prasad K.V.S.: A calculus of broadcasting systems. Sci. Comput. Program. 25(2-3), 285–327 (1995). doi:10.1016/0167-6423(95)00017-8
Ramachandran, K., Buddhikot, M.M., Chandranmenon, G., Miller, S., Belding-Royer, E.M., Almeroth, K.: On the design and implementation of infrastructure mesh networks. In: IEEE Workshop on Wireless Mesh Networks (WiMesh’05). IEEE (2005)
Rangarajan, H., Garcia-Luna-Aceves, J.J.: Making on-demand routing protocols based on destination sequence numbers robust. In: Communications (ICC ’05), vol. 5, pp. 3068–3072 (2005). doi:10.1109/ICC.2005.1494958
SCALABLE Network Technologies: QualNet communications simulation platform. http://web.scalable-networks.com/content/qualnet. Accessed 20 December 2013
Singh A., Ramakrishnan C.R., Smolka S.A.: A process calculus for mobile ad hoc networks. Sci. Comput. Program. 75, 440–469 (2010). doi:10.1016/j.scico.2009.07.008
Subramanian, A.P., Buddhikot, M.M., Miller, S.: Interference aware routing in multi-radio wireless mesh networks. In: IEEE Workshop on Wireless Mesh Networks (WiMesh ’06). IEEE (2006)
Tschudin, C.F.: Lightweight underlay network ad hoc routing (LUNAR) protocol. Internet Draft (Expired), Mobile Ad Hoc Networking Working Group (2004). http://user.it.uu.se/~rmg/pub/draft-tschudin-manet-lunar-00.txt
Tschudin, C.F., Gold, R., Rensfelt, O., Wibling, O.: LUNAR: a lightweight underlay network ad-hoc routing protocol and implementation. In: Koucheryavy, Y. Harju, J., Koucheryavy, A. (eds.) Next Generation Teletraffic and Wired/Wireless Advanced Networking (NEW2AN ’04) (2004)
van Glabbeek, R.J., Höfner, P., Tan, W.L., Portmann, M.: Sequence numbers do not guarantee loop freedom—AODV can yield routing loops. In: Modeling, Analysis and Simulation of Wireless and Mobile Systems (MSWiM ’13), pp. 91–100. ACM Press (2013). doi:10.1145/2507924.2507943
Yang H., Luo H., Ye F., Lu S., Zhang L.: Security in mobile ad hoc networks: challenges and solutions. IEEE Wirel. Commun. 11(1), 38–47 (2004). doi:10.1109/MWC.2004.1269716
Zave P.: Using lightweight modeling to understand chord. SIGCOMM Comput. Commun. Rev. 42(2), 49–57 (2012). doi:10.1145/2185376.2185383
Zhou, M., Yang, H., Zhang, X., Wang, J.: The proof of AODV loop freedom. In: Wireless Communications and Signal Processing (WCSP ’09). IEEE (2009). doi:10.1109/WCSP.2009.5371479
Author information
Authors and Affiliations
Corresponding author
Additional information
NICTA is funded by the Australian Government through the Department of Communications and the Australian Research Council through the ICT Centre of Excellence Program.
Rights and permissions
About this article
Cite this article
van Glabbeek, R., Höfner, P., Portmann, M. et al. Modelling and verifying the AODV routing protocol. Distrib. Comput. 29, 279–315 (2016). https://doi.org/10.1007/s00446-015-0262-7
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00446-015-0262-7