Skip to main content

Probabilistic Model Checking of AODV

  • Conference paper
  • First Online:
Quantitative Evaluation of Systems (QEST 2020)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 12289))

Included in the following conference series:

Abstract

This paper presents the formal modelling and verification of the Ad-hoc On-demand Distance Vector (AODV) routing protocol. Our study focuses on the quantitative aspects of AODV, in particular the influence of uncertainty (such as packet loss rates, collisions) on the probability to establish short routes. We present a compositional model of AODV’s functionality using probabilistic timed automata. The strength of this model is that it combines hard real-time constraints with randomised protocol behaviour and can deal with non-determinism (due to e.g., queue behaviours at network nodes). An automated analysis by probabilistic model checking provides useful insights on the sensitivity of AODV’s ability to establish shortest/longest routes and deliver data packets via such routes.

This work is funded by the German Research Foundation DFG.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    A digital clock semantics [35] where timer values are rounded to integral numbers gives rise to coarse finite abstractions.

  2. 2.

    In our model, collisions can still take place, despite the presence of collision avoidance protocols, and we deliberately decided to consider both collisions and message losses due to other causes separately.

  3. 3.

    When a message is broadcast or unicast, the message is immediately queued in the buffer of the recipient. This neither involves collisions nor MAC aspects.

  4. 4.

    https://git.rwth-aachen.de/mojgan.kamali/qest2020.

  5. 5.

    Due to limitation of MODEST in defining struct type, we define one array for every message element in the nodes’ buffer.

  6. 6.

    We do not verify our properties for Pmin as this probability is always 0 in our analysis.

  7. 7.

    In all of the topologies when all loss probabilities are 0%, the 1% probability of message collision(s) yields to a decrease in the probabilities of finding the short/long path (if any found) as well as the probability of packet delivery. This means that these probabilities are never 100% even in a fully reliable situation with all loss probabilities at 0% due to possible message collision(s) probability.

  8. 8.

    We also analysed an alternative variant of the protocol which not only checks for the rreq ID, but also if the message has arrived via a short path. Then, the node processes the message and rebroadcasts it. The results of our analysis show a seemingly contradictory results in this situation: when the loss probability increases on the short path, then the probability of finding the long path is monotonically increasing (in contrast to Fig. 8b). This shows that finding the longer path by AODV is somehow dependent on the increase/decrease of the loss probability on the short path in this setting.

References

  1. Agha, G., Palmskog, K.: A survey of statistical model checking. ACM Trans. Model. Comput. Simul. 28(1), 6:1–6:39 (2018)

    Article  MathSciNet  Google Scholar 

  2. Alsheikh, M.A., Hoang, D.T., Niyato, D., Tan, H.P., Lin, S.: Markov decision processes with applications in wireless sensor networks: a survey. IEEE Commun. Surv. Tutor. 17(3), 1239–1267 (2015)

    Article  Google Scholar 

  3. Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30080-9_7

    Chapter  Google Scholar 

  4. Biswas, A., Saha, B., Guha, S.: Performance analysis of AODV and DSR routing protocols for Ad-Hoc networks. In: Thilagam, P.S., Pais, A.R., Chandrasekaran, K., Balakrishnan, N. (eds.) ADCONS 2011. LNCS, vol. 7135, pp. 297–305. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-29280-4_36

    Chapter  Google Scholar 

  5. Bohnenkamp, H.C., D’Argenio, P.R., Hermanns, H., Katoen, J.: MODEST: a compositional modeling formalism for hard and softly timed systems. IEEE Trans. Software Eng. 32(10), 812–830 (2006)

    Article  Google Scholar 

  6. Cavin, D., Sasson, Y., Schiper, A.: On the accuracy of MANET simulators. In: POMC, pp. 38–43. ACM (2002)

    Google Scholar 

  7. Chakeres, I.D., Belding-Royer, E.M.: AODV routing protocol implementation design. In: Proceedings of the 24th International Conference on Distributed Computing Systems Workshops, 2004, pp. 698–703 (2004)

    Google Scholar 

  8. Chaudhary, K., Fehnker, A., Mehta, V.: Modelling, verification, and comparative performance analysis of the B.A.T.M.A.N. protocol. In: MARS, EPTCS, vol. 244, pp. 53–65 (2017)

    Google Scholar 

  9. Chavan, A., Kurule, D., Dere, P.: Performance analysis of AODV and DSDV routing protocol in MANET and modifications in AODV against black hole attack. Procedia Comput. Sci. 79, 835–844 (2016)

    Article  Google Scholar 

  10. Chiyangwa, S., Kwiatkowska, M.: A timing analysis of AODV. In: Steffen, M., Zavattaro, G. (eds.) FMOODS 2005. LNCS, vol. 3535, pp. 306–321. Springer, Heidelberg (2005). https://doi.org/10.1007/11494881_20

    Chapter  Google Scholar 

  11. Dal Corso, A., Macedonio, D., Merro, M.: Statistical model checking of ad hoc routing protocols in lossy grid networks. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 112–126. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-17524-9_9

    Chapter  Google Scholar 

  12. David, A., Larsen, K.G., Legay, A., Mikučionis, M., Poulsen, D.B.: Uppaal SMC tutorial. Int. J. Softw. Tools Tech. Trans. 17(4), 397–415 (2015)

    Article  Google Scholar 

  13. Dombrowski, C., Junges, S., Katoen, J., Gross, J.: Model-checking assisted protocol design for ultra-reliable low-latency wireless networks. In: IEEE 35th Symposium on Reliable Distributed Systems (SRDS), pp. 307–316. IEEE (2016)

    Google Scholar 

  14. Fehnker, A., van Glabbeek, R., Höfner, P., McIver, A., Portmann, M., Tan, W.L.: Automated analysis of AODV using UPPAAL. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 173–187. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-28756-5_13

    Chapter  MATH  Google Scholar 

  15. Fehnker, A., van Hoesel, L., Mader, A.: Modelling and verification of the LMAC protocol for wireless sensor networks. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol. 4591, pp. 253–272. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73210-5_14

    Chapter  Google Scholar 

  16. Garg, S., Verma, A.K.: Simulation and comparison of AODV variants under different mobility models in MANETs. In: Vishwakarma, H.R., Akashe, S. (eds.) Computing and Network Sustainability. LNNS, vol. 12, pp. 333–342. Springer, Singapore (2017). https://doi.org/10.1007/978-981-10-3935-5_34

    Chapter  Google Scholar 

  17. van Glabbeek, R., Höfner, P., Portmann, M., Tan, W.L.: Modelling and verifying the AODV routing protocol. Distrib. Comput. 29(4), 279–315 (2016). https://doi.org/10.1007/s00446-015-0262-7

    Article  MathSciNet  MATH  Google Scholar 

  18. Groß, C., Hermanns, H., Pulungan, R.: Does clock precision influence Zigbee’s energy consumptions? In: Tovar, E., Tsigas, P., Fouchal, H. (eds.) OPODIS 2007. LNCS, vol. 4878, pp. 174–188. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-77096-1_13

    Chapter  Google Scholar 

  19. Hahn, E.M., Hartmanns, A., Hermanns, H., Katoen, J.P.: A compositional modelling and analysis framework for stochastic hybrid systems. Formal Methods Syst. Design 43(2), 191–232 (2013). https://doi.org/10.1007/s10703-012-0167-z

    Article  MATH  Google Scholar 

  20. Hartmanns, A., Hermanns, H.: A Modest approach to checking probabilistic timed automata. In: QEST, pp. 187–196. IEEE (2009)

    Google Scholar 

  21. Hartmanns, A., Hermanns, H.: The modest toolset: an integrated environment for quantitative modelling and verification. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 593–598. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54862-8_51

    Chapter  Google Scholar 

  22. Hoebeke, J., Moerman, I., Dhoedt, B., Demeester, P.: An overview of mobile ad hoc networks: applications and challenges. Commun. Netw. 3, 60–66 (2004)

    Google Scholar 

  23. Höfner, P., McIver, A.: Statistical model checking of wireless mesh routing protocols. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 322–336. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38088-4_22

    Chapter  Google Scholar 

  24. Höfner, P., Kamali, M.: Quantitative analysis of AODV and its variants on dynamic topologies using statistical model checking. In: Braberman, V., Fribourg, L. (eds.) FORMATS 2013. LNCS, vol. 8053, pp. 121–136. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-40229-6_9

    Chapter  Google Scholar 

  25. Kamali, M., Fehnker, A.: Adaptive formal framework for WMN routing protocols. In: Bae, K., Ölveczky, P.C. (eds.) FACS 2018. LNCS, vol. 11222, pp. 175–195. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-02146-7_9

    Chapter  Google Scholar 

  26. Kamali, M., Höfner, P., Kamali, M., Petre, L.: Formal analysis of proactive, distributed routing. In: Calinescu, R., Rumpe, B. (eds.) SEFM 2015. LNCS, vol. 9276, pp. 175–189. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-22969-0_13

    Chapter  Google Scholar 

  27. Kamali, M., Merro, M., Dal Corso, A.: AODVv2: performance vs. loop freedom. In: Tjoa, A.M., Bellatreche, L., Biffl, S., van Leeuwen, J., Wiedermann, J. (eds.) SOFSEM 2018. LNCS, vol. 10706, pp. 337–350. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-73117-9_24

    Chapter  Google Scholar 

  28. Katoen, J.: The probabilistic model checking landscape. In: LICS, pp. 31–45. ACM (2016)

    Google Scholar 

  29. Kolipaka, S., Bhandari, B.N., Rajani, A.: Performance analysis of AODV with multi-radio in hybrid wireless mesh network. In: Eleventh International Conference on Wireless and Optical Communications Networks (WOCN), pp. 1–5. IEEE (2014)

    Google Scholar 

  30. Kwak, B.J., Song, N.O., Miller, L.E.: Performance analysis of exponential backoff. IEEE/ACM Trans. Network. 13(2), 343–355 (2005)

    Article  Google Scholar 

  31. Kwiatkowska, M.Z., Norman, G., Segala, R., Sproston, J.: Automatic verification of real-time systems with discrete probability distributions. Theor. Comput. Sci. 282(1), 101–150 (2002)

    Article  MathSciNet  Google Scholar 

  32. Misic, J., Shafi, S., Misic, V.B.: Performance of a beacon enabled IEEE 802.15.4 cluster with downlink and uplink traffic. IEEE Trans. Parallel Distrib. Syst. 17(4), 361–376 (2006)

    Article  Google Scholar 

  33. Negra, R., Jemili, I., Belghith, A.: Wireless body area networks: applications and technologies. Procedia Comput. Sci. 83, 1274–1281 (2016)

    Article  Google Scholar 

  34. Neumann, A., Aichele, C., Lindner, M., Wunderlich, S.: Better approach to mobile ad-hoc networking (BATMAN). Internet draft00 (2008). https://tools.ietf.org/html/draft-wunderlich-openmesh-manet-routing-00

  35. Norman, G., Parker, D., Sproston, J.: Model checking for probabilistic timed automata. Formal Methods Syst. Des. 43(2), 164–190 (2013). https://doi.org/10.1007/s10703-012-0177-x

    Article  MATH  Google Scholar 

  36. Obaidat, M.S., Green, D.B.: Simulation of wireless networks. In: Obaidat, M.S., Papadimitriou, G.I. (eds.) Applied System Simulation. Springer, Boston (2003). https://doi.org/10.1007/978-1-4419-9218-5_6

    Chapter  Google Scholar 

  37. Perkins, C., Stan, R., Dowdell, J., Steenbrink, L., Mercieca, V.: DynamicMANET On-demand (AODVv2) Routing draft-ietf-manet-aodvv2. Internet Draft 2016 (2016)

    Google Scholar 

  38. Perkins, C., Belding-Royer, E., Das, S.: Ad hoc on-demand distance vector (AODV) routing. RFC 3561 (2003). https://www.ietf.org/rfc/rfc3561

  39. Perkins, C., Stan, R., Dowdell, J.: Dynamic manet on-demand (AODVv2) routing draft-ietf-manet-dymo. Internat draft26 (2013). https://tools.ietf.org/html/draft-ietf-manet-dymo-26

  40. Schemmel, D., Büning, J., Soria Dustmann, O., Noll, T., Wehrle, K.: Symbolic liveness analysis of real-world software. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 447–466. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-96142-2_27

    Chapter  Google Scholar 

  41. Shao, C., Hui, D., Pazhyannur, R., Bari, F., Zhang, R., Matsushima, S.: IEEE 802.11 medium access control (MAC) profile for control and provisioning of wireless access points (CAPWAP). RFC 7494 (2015). https://tools.ietf.org/html/rfc7494

  42. Suriyachai, P., Roedig, U., Scott, A.: A survey of MAC protocols for mission-critical applications in wireless sensor networks. IEEE Commun. Surv. Tutor. 14(2), 240–264 (2012)

    Article  Google Scholar 

Download references

Acknowledgment

We thank Peter Höfner (ANU) for discussions on AODV, Arnd Hartmanns (Twente) for assistance using mcsta and the reviewers for their helpful comments.

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Mojgan Kamali .

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2020 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Kamali, M., Katoen, JP. (2020). Probabilistic Model Checking of AODV. In: Gribaudo, M., Jansen, D.N., Remke, A. (eds) Quantitative Evaluation of Systems. QEST 2020. Lecture Notes in Computer Science(), vol 12289. Springer, Cham. https://doi.org/10.1007/978-3-030-59854-9_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-59854-9_6

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-59853-2

  • Online ISBN: 978-3-030-59854-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics