Statistical Model Checking of Ad Hoc Routing Protocols in Lossy Grid Networks

  • Alice Dal Corso
  • Damiano Macedonio
  • Massimo MerroEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9058)


We extend recent work by Höfner and McIver con the performances of the ad hoc routing protocols AODV and DYMO in terms of routes established. Höfner and McIver apply statistical model checking to show that on arbitrary small networks (up to 5 nodes) the most recent, and apparently more robust, DYMO protocol is less efficient than AODV. Here, we reformulate their experiments on 4x3 toroidal networks, with possibly lossy communication. As a main result we demonstrate that, in this more realistic scenario, DYMO performs significantly better than AODV.


Destination Node Optimal Route Route Discovery Route Request Optimize Link State Route 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Behrmann, G., David, A., Larsen, K.G., Håkansson, J., Pettersson, P., Yi, W., Hendriks, M.: UPPAAL 4.0. In: International Conference on the Quantitative Evaluation of Systems (QEST), pp. 125–126. IEEE Computer Society (2006)Google Scholar
  2. 2.
    Benetti, D., Merro, M., Vigano, L.: Model checking ad hoc network routing protocols: Aran vs. endairA. In: 8th IEEE International Conference on Software Engineering and Formal Methods (SEFM), pp. 191–202. IEEE Computer Society (2010)Google Scholar
  3. 3.
    Bhargavan, K., Obradovic, D., Gunter, C.: Formal verification of standards for distance vector routing protocols. Journal of the ACM 49, 538–576 (2002)CrossRefMathSciNetGoogle Scholar
  4. 4.
    Bulychev, P., David, A., Guldstrand Larsen, K., Legay, A., Mikučionis, M., Bøgsted Poulsen, D.: Checking and distributing statistical model checking. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 449–463. Springer, Heidelberg (2012) CrossRefGoogle Scholar
  5. 5.
    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) CrossRefGoogle Scholar
  6. 6.
    Clausen, T., Jacquet, P.: Optimized Link State Routing Protocol (OLSR), rFC 3626 (2003)Google Scholar
  7. 7.
    David, A., Larsen, K.G., Legay, A., Mikučionis, M., Poulsen, D.B., van Vliet, J., Wang, Z.: Statistical model checking for networks of priced timed automata. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol. 6919, pp. 80–96. Springer, Heidelberg (2011) CrossRefGoogle Scholar
  8. 8.
    David, A., Larsen, K.G., Legay, A., Mikučionis, M., Wang, Z.: Time for statistical model checking of real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 349–355. Springer, Heidelberg (2011) CrossRefGoogle Scholar
  9. 9.
    Edenhofer, S., Höfner, P.: Towards a rigorous analysis of AODVv2 (DYMO). In: IEEE International Conference on Network Protocols (ICNP), pp. 1–6. IEEE Computer Society (2012)Google Scholar
  10. 10.
    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) CrossRefGoogle Scholar
  11. 11.
    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) CrossRefGoogle Scholar
  12. 12.
    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) CrossRefGoogle Scholar
  13. 13.
    Johnson, D.B., Maltz, D.A.: Dynamic Source Routing in Ad Hoc Wireless Networks. Kluwer Acad. Pub. (1996)Google Scholar
  14. 14.
    Liu, S., Ölveczky, P.C., Meseguer, J.: A framework for mobile Ad hoc networks in real-time maude. In: Escobar, S. (ed.) WRLA 2014. LNCS, vol. 8663, pp. 162–177. Springer, Heidelberg (2014) CrossRefGoogle Scholar
  15. 15.
    Merro, M., Sibilio, E.: A calculus of trustworthy ad hoc networks. Formal Aspects of Computing 25(5), 801–832 (2013)CrossRefzbMATHMathSciNetGoogle Scholar
  16. 16.
    Miskovic, S., Knightly, E.: Routing primitives for wireless mesh networks: design, analysis and experiments. In: IEEE International Conference on Computer Communications (INFOCOM), pp. 2793–2801. IEEE Computer Society (2010)Google Scholar
  17. 17.
    Perkins, C., Belding-Royer, E., Das, S.: Ad-hoc on-demand distance vector (AODV). RFC 3561 (Experimental) (2003).
  18. 18.
    Perkins, C., Chakeres, I.: Dynamic MANET on-demand (AODVv2) routing. IETF Internet Draft (2012, Work in Progress)Google Scholar
  19. 19.
    Perkins, C.E., Bhagwat, P.: Highly dynamic destination-sequenced distance-vector routing (DSDV) for mobile computers. In: Conference on Communications Architectures, Protocols and Applications (SIGCOMM), pp. 234–244 (1994)Google Scholar
  20. 20.
    Sen, K., Viswanathan, M., Agha, G.: VESTA: A statistical model-checker and analyzer for probabilistic systems. In: International Conference on the Quantitative Evaluation of Systems (QEST), pp. 251–252. IEEE Computer Society (2005)Google Scholar
  21. 21.
    Younes, H., S.: Verification and Planning for Stochastic Processes with Asynchronous Events. Ph.D. thesis, Carnegie Mellon University (2004)Google Scholar

Copyright information

© Springer International Publishing Switzerland 2015

Authors and Affiliations

  • Alice Dal Corso
    • 1
  • Damiano Macedonio
    • 2
  • Massimo Merro
    • 1
    Email author
  1. 1.Dipartimento di InformaticaUniversità degli Studi di VeronaVeronaItaly
  2. 2.Julia SrlVeronaItaly

Personalised recommendations