Trustworthy Systems

Statistical model checking of wireless mesh routing protocols

Authors

Peter Hoefner and Annabelle McIver

NICTA

UNSW

Macquarie University

Abstract

Several case studies indicate that model checking is limited in the analysis of mesh networks: state space explosion restricts applicability to at most 10 node networks, and quantitative reasoning, often sufficient for network evaluation, is not possible. Both deficiencies can be overcome to some extent by the use of statistical model checkers, such as SMC-Uppaal. In this paper we illustrate this by a quantitative analysis of two well-known routing protocols for wireless mesh networks, namely AODV and DYMO. Moreover, we push the limits and show that this technology is capable of analysing networks of up to 100 nodes.

BibTeX Entry

  @inproceedings{Hoefner_McIver_13,
    address          = {Moffett Field, CA, USA},
    author           = {H\"ofner, Peter and McIver, Annabelle},
    booktitle        = {5th NASA Formal Methods Symposium (NFM 2013)},
    editor           = {{G. Brat, N. Rungta, and A. Venet}},
    keywords         = {statistical model checking; wireless routing protocols; quantitative analysis},
    month            = may,
    pages            = {15},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/6542.pdf},
    publisher        = {Springer},
    title            = {Statistical Model Checking of Wireless Mesh Routing Protocols},
    year             = {2013}
  }

Download