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
Fehnker, Ansgar ; Fehnker, Ansgar ; van Hoesel, L.F.W. ; Mader, Angelika H. / Modelling and Verification of the LMAC Protocol for Wireless Sensor Networks. Proceedings of the 6th International Conference on Integrated Formal Methods, IFM 2007. editor / Jim Davis ; Jeremy Gibbons. Berlin / Heidelberg : Springer, 2007. pp. 253-272 (Lecture Notes in Computer Science; 7).
@inproceedings{08ab025f2b3f412cb2337f83bc3d4a77,
title = "Modelling and Verification of the LMAC Protocol for Wireless Sensor Networks",
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.",
keywords = "CAES-PS: Pervasive Systems, CR-F.3.1, IR-62160, METIS-246008, EWI-11888",
author = "Ansgar Fehnker and Ansgar Fehnker and {van Hoesel}, L.F.W. and Mader, {Angelika H.}",
note = "10.1007/978-3-540-73210-5_14",
year = "2007",
month = "6",
doi = "10.1007/978-3-540-73210-5_14",
language = "Undefined",
isbn = "978-3-540-73209-9",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
number = "7",
pages = "253--272",
editor = "Jim Davis and Jeremy Gibbons",
booktitle = "Proceedings of the 6th International Conference on Integrated Formal Methods, IFM 2007",

}

Fehnker, A, Fehnker, A, van Hoesel, LFW & Mader, AH 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., 10.1007/978-3-540-73210-5_14, Lecture Notes in Computer Science, no. 7, vol. 4591, Springer, Berlin / Heidelberg, pp. 253-272. https://doi.org/10.1007/978-3-540-73210-5_14

Modelling and Verification of the LMAC Protocol for Wireless Sensor Networks. / Fehnker, Ansgar; Fehnker, Ansgar; van Hoesel, L.F.W.; Mader, Angelika H.

Proceedings of the 6th International Conference on Integrated Formal Methods, IFM 2007. ed. / Jim Davis; Jeremy Gibbons. Berlin / Heidelberg : Springer, 2007. p. 253-272 10.1007/978-3-540-73210-5_14 (Lecture Notes in Computer Science; Vol. 4591, No. 7).

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

TY - GEN

T1 - Modelling and Verification of the LMAC Protocol for Wireless Sensor Networks

AU - Fehnker, Ansgar

AU - Fehnker, Ansgar

AU - van Hoesel, L.F.W.

AU - Mader, Angelika H.

N1 - 10.1007/978-3-540-73210-5_14

PY - 2007/6

Y1 - 2007/6

N2 - 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.

AB - 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.

KW - CAES-PS: Pervasive Systems

KW - CR-F.3.1

KW - IR-62160

KW - METIS-246008

KW - EWI-11888

U2 - 10.1007/978-3-540-73210-5_14

DO - 10.1007/978-3-540-73210-5_14

M3 - Conference contribution

SN - 978-3-540-73209-9

T3 - Lecture Notes in Computer Science

SP - 253

EP - 272

BT - Proceedings of the 6th International Conference on Integrated Formal Methods, IFM 2007

A2 - Davis, Jim

A2 - Gibbons, Jeremy

PB - Springer

CY - Berlin / Heidelberg

ER -

Fehnker A, Fehnker A, van Hoesel LFW, Mader AH. Modelling and Verification of the LMAC Protocol for Wireless Sensor Networks. In Davis J, Gibbons J, editors, Proceedings of the 6th International Conference on Integrated Formal Methods, IFM 2007. Berlin / Heidelberg: Springer. 2007. p. 253-272. 10.1007/978-3-540-73210-5_14. (Lecture Notes in Computer Science; 7). https://doi.org/10.1007/978-3-540-73210-5_14