Statistical model checking of wireless mesh routing protocols

Peter Höfner, Annabelle McIver

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contribution

15 Citations (Scopus)


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.

Original languageEnglish
Title of host publicationNASA Formal Methods - 5th International Symposium, NFM 2013, Proceedings
EditorsGuillaume Brat, Neha Rungta, Arnaud Venet
Place of PublicationHeidelberg
PublisherSpringer, Springer Nature
Number of pages15
ISBN (Print)9783642380877
Publication statusPublished - 2013
Event5th International Symposium on NASA Formal Methods, NFM 2013 - Moffett Field, CA, United States
Duration: 14 May 201316 May 2013

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7871 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349


Other5th International Symposium on NASA Formal Methods, NFM 2013
CountryUnited States
CityMoffett Field, CA

Fingerprint Dive into the research topics of 'Statistical model checking of wireless mesh routing protocols'. Together they form a unique fingerprint.

Cite this