Modelling and Verification of the LMAC Protocol for Wireless Sensor Networks

Ansgar Fehnker; Lodewijk van Hoesel; Angelika H. 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 H. Mader

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

10 Downloads (Pure)

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 Davis, Jeremy Gibbons
Place of Publication	Berlin, Heidelberg
Publisher	Springer
Pages	253-272
Number of pages	20
ISBN (Electronic)	978-3-540-73210-5
ISBN (Print)	978-3-540-73209-9
DOIs	https://doi.org/10.1007/978-3-540-73210-5_14
Publication status	Published - Jun 2007
Event	6th International Conference on Integrated Formal Methods, IFM 2007: Proceedings of the 6th International Conference on Integrated Formal Methods, IFM 2007 - Oxford, Britain, Berlin / Heidelberg Duration: 2 Jul 2007 → 5 Jul 2007

Publication series

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

Conference

Conference	6th International Conference on Integrated Formal Methods, IFM 2007
City	Berlin / Heidelberg
Period	2/07/07 → 5/07/07
Other	2-5 July 2007

Keywords

CAES-PS: Pervasive Systems
CR-F.3.1

Access to Document

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

Cite this

Fehnker, A., van Hoesel, L., & Mader, A. H. (2007). Modelling and Verification of the LMAC Protocol for Wireless Sensor Networks. In J. Davis, & 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. https://doi.org/10.1007/978-3-540-73210-5_14

Fehnker, Ansgar ; van Hoesel, Lodewijk ; Mader, Angelika H. / 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 Davis ; Jeremy Gibbons. Berlin, Heidelberg : Springer, 2007. pp. 253-272 (Lecture Notes in Computer Science).

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

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

year = "2007",

month = jun,

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

language = "English",

isbn = "978-3-540-73209-9",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "253--272",

editor = "Jim Davis and Jeremy Gibbons",

booktitle = "Integrated Formal Methods",

address = "Germany",

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

}

Fehnker, A, van Hoesel, L & Mader, AH 2007, Modelling and Verification of the LMAC Protocol for Wireless Sensor Networks. in J Davis & 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, Berlin, Heidelberg, pp. 253-272, 6th International Conference on Integrated Formal Methods, IFM 2007, Berlin / Heidelberg, 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 H.
Integrated Formal Methods: 6th International Conference, IFM 2007, Oxford, UK, July 2-5, 2007. Proceedings. ed. / Jim Davis; Jeremy Gibbons. Berlin, Heidelberg: Springer, 2007. p. 253-272 (Lecture Notes in Computer Science; Vol. 4591).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › 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 H.

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

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 - Integrated Formal Methods

A2 - Davis, Jim

A2 - Gibbons, Jeremy

PB - Springer

CY - Berlin, Heidelberg

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 AH. Modelling and Verification of the LMAC Protocol for Wireless Sensor Networks. In Davis J, Gibbons J, editors, Integrated Formal Methods: 6th International Conference, IFM 2007, Oxford, UK, July 2-5, 2007. Proceedings. Berlin, Heidelberg: Springer. 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

Conference

Keywords

Access to Document

Fingerprint

Cite this