Modelling and Verification of the LMAC Protocol for Wireless Sensor Networks

Ansgar Fehnker, Lodewijk van Hoesel, Angelika Mader

    Research output: Book/ReportReportProfessional

    69 Citations (Scopus)
    96 Downloads (Pure)


    In this paper we report about modelling and verification of a medium access control protocol for wireless sensor networks, the LMAC protocol. Our approach is to systematically investigate all possible con- nected topologies consisting of four and of five nodes. The analysis is performed by timed automaton model checking using Uppaal. The prop- erty of main interest is detecting and resolving collision. To evaluate this property for all connected topologies more than 8000 model checking runs were required. Increasing the number of nodes would not lead only to state space problem, but to much more extent cause an instance ex- plosion 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 ad- equacy of the protocol.
    Original languageEnglish
    Place of PublicationEnschede
    PublisherCentre for Telematics and Information Technology (CTIT)
    Number of pages20
    Publication statusPublished - 6 Feb 2007

    Publication series

    NameCTIT Technical Report Series
    PublisherCentre for Telematics and Information Technology, University of Twente
    ISSN (Print)1381-3625


    • 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