Modelling and Verification of the LMAC Protocol for Wireless Sensor Networks

Ansgar Fehnker, Ansgar Fehnker, L.F.W. van Hoesel, Angelika H. Mader

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

    Abstract

    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 languageUndefined
    Title of host publicationProceedings of the 6th International Conference on Integrated Formal Methods, IFM 2007
    EditorsJim Davis, Jeremy Gibbons
    Place of PublicationBerlin / Heidelberg
    PublisherSpringer
    Pages253-272
    Number of pages20
    ISBN (Print)978-3-540-73209-9
    DOIs
    Publication statusPublished - Jun 2007

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer Verlag
    Number7
    Volume4591
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Keywords

    • CAES-PS: Pervasive Systems
    • CR-F.3.1
    • IR-62160
    • METIS-246008
    • EWI-11888

    Cite this

    Fehnker, A., Fehnker, A., van Hoesel, L. F. W., & Mader, A. H. (2007). Modelling and Verification of the LMAC Protocol for Wireless Sensor Networks. In J. Davis, & J. Gibbons (Eds.), Proceedings of the 6th International Conference on Integrated Formal Methods, IFM 2007 (pp. 253-272). [10.1007/978-3-540-73210-5_14] (Lecture Notes in Computer Science; Vol. 4591, No. 7). Berlin / Heidelberg: Springer. https://doi.org/10.1007/978-3-540-73210-5_14