Trustworthy Systems

Statistical model checking of wireless mesh routing protocols


Peter Hoefner and Annabelle McIver



Macquarie University


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

    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         = {},
    publisher        = {Springer},
    title            = {Statistical Model Checking of Wireless Mesh Routing Protocols},
    year             = {2013}