Modelling and verification of the LMAC protocol for wireless sensor networks

Ansgar Fehnker, Lodewijk van Hoesel, Angelika Mader

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contributionpeer-review

70 Citations (Scopus)


In this paper we report on modelling and verification of a medium access control protocol for wireless sensor networks, the LMAC protocol. Our approach is to systematically investigate all possible connected topologies consisting of four and of five nodes. The analysis is performed by timed automaton model checking using Uppaal. The property of main interest is detecting and resolving collision. Evaluation of this property for all connected topologies requires more than 8000 model checking runs. Increasing the number of nodes would not only lead increase the state space, but to a greater extent cause an instance explosion problem. Despite the small number of nodes this approach gave valuable insight in the protocol and the scenarios that lead to collisions not detected by the protocol, and it increased the confidence in the adequacy of the protocol.
Original languageEnglish
Title of host publicationIntegrated Formal Methods
Subtitle of host publication6th International Conference, IFM 2007 Oxford, UK, July 2-5, 2007, Proceedings
EditorsJim Davies, Jeremy Gibbons
Place of PublicationBerlin
PublisherSpringer, Springer Nature
Number of pages20
ISBN (Print)9783540732099, 3540732098
Publication statusPublished - 2007
Externally publishedYes
Event6th International Conference on Integrated Formal Methods, IFM 2007 - Oxford, United Kingdom
Duration: 2 Jul 20075 Jul 2007

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743


Other6th International Conference on Integrated Formal Methods, IFM 2007
Country/TerritoryUnited Kingdom


  • CAES-PS: Pervasive Systems


Dive into the research topics of 'Modelling and verification of the LMAC protocol for wireless sensor networks'. Together they form a unique fingerprint.

Cite this