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 Verlag
Pages253-272
Number of pages20
ISBN (Print)978-3-540-73209-9
DOIs
StatePublished - Jun 2007

Publication series

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

Fingerprint

Model checking
Topology
Medium access control
Explosions
Wireless sensor networks

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 Verlag. DOI: 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. ed. / Jim Davis; Jeremy Gibbons. Berlin / Heidelberg : Springer Verlag, 2007. p. 253-272 10.1007/978-3-540-73210-5_14 (Lecture Notes in Computer Science; Vol. 4591, No. 7).

Research output: Scientific - peer-reviewConference contribution

@inbook{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",
isbn = "978-3-540-73209-9",
series = "Lecture Notes in Computer Science",
publisher = "Springer Verlag",
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 Verlag, Berlin / Heidelberg, pp. 253-272. DOI: 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 Verlag, 2007. p. 253-272 10.1007/978-3-540-73210-5_14 (Lecture Notes in Computer Science; Vol. 4591, No. 7).

Research output: Scientific - peer-reviewConference contribution

TY - CHAP

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

PB - Springer Verlag

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 Verlag. 2007. p. 253-272. 10.1007/978-3-540-73210-5_14. (Lecture Notes in Computer Science; 7). Available from, DOI: 10.1007/978-3-540-73210-5_14