Modelling and verification of the LMAC protocol for wireless sensor networks

Ansgar Fehnker; Lodewijk van Hoesel; Angelika Mader

doi:10.1007/978-3-540-73210-5_14

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 proceeding › Conference proceeding contribution › peer-review

71 Citations (Scopus)

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 language	English
Title of host publication	Integrated Formal Methods
Subtitle of host publication	6th International Conference, IFM 2007 Oxford, UK, July 2-5, 2007, Proceedings
Editors	Jim Davies, Jeremy Gibbons
Place of Publication	Berlin
Publisher	Springer, Springer Nature
Pages	253-272
Number of pages	20
ISBN (Print)	9783540732099, 3540732098
DOIs	https://doi.org/10.1007/978-3-540-73210-5_14
Publication status	Published - 2007
Externally published	Yes
Event	6th International Conference on Integrated Formal Methods, IFM 2007 - Oxford, United Kingdom Duration: 2 Jul 2007 → 5 Jul 2007

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	4591
ISSN (Print)	0302-9743

Other

Other	6th International Conference on Integrated Formal Methods, IFM 2007
Country/Territory	United Kingdom
City	Oxford
Period	2/07/07 → 5/07/07

Keywords

CAES-PS: Pervasive Systems

Access to Document

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

Cite this

Fehnker, A., van Hoesel, L., & Mader, A. (2007). Modelling and verification of the LMAC protocol for wireless sensor networks. In J. Davies, & J. Gibbons (Eds.), Integrated Formal Methods: 6th International Conference, IFM 2007 Oxford, UK, July 2-5, 2007, Proceedings (pp. 253-272). (Lecture Notes in Computer Science; Vol. 4591). Springer, Springer Nature. https://doi.org/10.1007/978-3-540-73210-5_14

Fehnker, Ansgar ; van Hoesel, Lodewijk ; Mader, Angelika. / Modelling and verification of the LMAC protocol for wireless sensor networks. Integrated Formal Methods: 6th International Conference, IFM 2007 Oxford, UK, July 2-5, 2007, Proceedings. editor / Jim Davies ; Jeremy Gibbons. Berlin : Springer, Springer Nature, 2007. pp. 253-272 (Lecture Notes in Computer Science).

@inproceedings{d061a0d2ed07452a9a6991285a4ce48f,

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",

author = "Ansgar Fehnker and {van Hoesel}, Lodewijk and Angelika Mader",

year = "2007",

doi = "10.1007/978-3-540-73210-5_14",

language = "English",

isbn = "9783540732099",

series = "Lecture Notes in Computer Science",

publisher = "Springer, Springer Nature",

pages = "253--272",

editor = "Jim Davies and Jeremy Gibbons",

booktitle = "Integrated Formal Methods",

address = "United States",

note = "6th International Conference on Integrated Formal Methods, IFM 2007 ; Conference date: 02-07-2007 Through 05-07-2007",

}

Fehnker, A, van Hoesel, L & Mader, A 2007, Modelling and verification of the LMAC protocol for wireless sensor networks. in J Davies & J Gibbons (eds), Integrated Formal Methods: 6th International Conference, IFM 2007 Oxford, UK, July 2-5, 2007, Proceedings. Lecture Notes in Computer Science, vol. 4591, Springer, Springer Nature, Berlin, pp. 253-272, 6th International Conference on Integrated Formal Methods, IFM 2007, Oxford, United Kingdom, 2/07/07. https://doi.org/10.1007/978-3-540-73210-5_14

Modelling and verification of the LMAC protocol for wireless sensor networks. / Fehnker, Ansgar; van Hoesel, Lodewijk; Mader, Angelika.
Integrated Formal Methods: 6th International Conference, IFM 2007 Oxford, UK, July 2-5, 2007, Proceedings. ed. / Jim Davies; Jeremy Gibbons. Berlin: Springer, Springer Nature, 2007. p. 253-272 (Lecture Notes in Computer Science; Vol. 4591).

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding contribution › peer-review

TY - GEN

T1 - Modelling and verification of the LMAC protocol for wireless sensor networks

AU - Fehnker, Ansgar

AU - van Hoesel, Lodewijk

AU - Mader, Angelika

PY - 2007

Y1 - 2007

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

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

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

M3 - Conference proceeding contribution

SN - 9783540732099

SN - 3540732098

T3 - Lecture Notes in Computer Science

SP - 253

EP - 272

BT - Integrated Formal Methods

A2 - Davies, Jim

A2 - Gibbons, Jeremy

PB - Springer, Springer Nature

CY - Berlin

T2 - 6th International Conference on Integrated Formal Methods, IFM 2007

Y2 - 2 July 2007 through 5 July 2007

ER -

Fehnker A, van Hoesel L, Mader A. Modelling and verification of the LMAC protocol for wireless sensor networks. In Davies J, Gibbons J, editors, Integrated Formal Methods: 6th International Conference, IFM 2007 Oxford, UK, July 2-5, 2007, Proceedings. Berlin: Springer, Springer Nature. 2007. p. 253-272. (Lecture Notes in Computer Science). doi: 10.1007/978-3-540-73210-5_14

Modelling and verification of the LMAC protocol for wireless sensor networks

Abstract

Publication series

Other

Keywords

Access to Document

Fingerprint

Cite this