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: Book/ReportReportProfessional

60 Citations (Scopus)
63 Downloads (Pure)

Abstract

In this paper we report about modelling and verification of a medium access control protocol for wireless sensor networks, the LMAC protocol. Our approach is to systematically investigate all possible con- nected topologies consisting of four and of five nodes. The analysis is performed by timed automaton model checking using Uppaal. The prop- erty of main interest is detecting and resolving collision. To evaluate this property for all connected topologies more than 8000 model checking runs were required. Increasing the number of nodes would not lead only to state space problem, but to much more extent cause an instance ex- plosion 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 ad- equacy of the protocol.
Original languageUndefined
Place of PublicationEnschede
PublisherDistributed and Embedded Security (DIES)
Number of pages20
Publication statusPublished - 6 Feb 2007

Publication series

NameCTIT Technical Report Series
PublisherCentre for Telematics and Information Technology, University of Twente
No.TR-CTIT-07-09
ISSN (Print)1381-3625

Keywords

  • METIS-242160
  • CAES-PS: Pervasive Systems
  • EWI-9447
  • IR-66987

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. (CTIT Technical Report Series; No. TR-CTIT-07-09). Enschede: Distributed and Embedded Security (DIES).
Fehnker, Ansgar ; Fehnker, Ansgar ; van Hoesel, L.F.W. ; Mader, Angelika H. / Modelling and Verification of the LMAC Protocol for Wireless Sensor Networks. Enschede : Distributed and Embedded Security (DIES), 2007. 20 p. (CTIT Technical Report Series; TR-CTIT-07-09).
@book{bfc94a0380fb48fbb646eb83cc3bd7f4,
title = "Modelling and Verification of the LMAC Protocol for Wireless Sensor Networks",
abstract = "In this paper we report about modelling and verification of a medium access control protocol for wireless sensor networks, the LMAC protocol. Our approach is to systematically investigate all possible con- nected topologies consisting of four and of five nodes. The analysis is performed by timed automaton model checking using Uppaal. The prop- erty of main interest is detecting and resolving collision. To evaluate this property for all connected topologies more than 8000 model checking runs were required. Increasing the number of nodes would not lead only to state space problem, but to much more extent cause an instance ex- plosion 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 ad- equacy of the protocol.",
keywords = "METIS-242160, CAES-PS: Pervasive Systems, EWI-9447, IR-66987",
author = "Ansgar Fehnker and Ansgar Fehnker and {van Hoesel}, L.F.W. and Mader, {Angelika H.}",
year = "2007",
month = "2",
day = "6",
language = "Undefined",
series = "CTIT Technical Report Series",
publisher = "Distributed and Embedded Security (DIES)",
number = "TR-CTIT-07-09",

}

Fehnker, A, Fehnker, A, van Hoesel, LFW & Mader, AH 2007, Modelling and Verification of the LMAC Protocol for Wireless Sensor Networks. CTIT Technical Report Series, no. TR-CTIT-07-09, Distributed and Embedded Security (DIES), Enschede.

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

Enschede : Distributed and Embedded Security (DIES), 2007. 20 p. (CTIT Technical Report Series; No. TR-CTIT-07-09).

Research output: Book/ReportReportProfessional

TY - BOOK

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.

PY - 2007/2/6

Y1 - 2007/2/6

N2 - In this paper we report about modelling and verification of a medium access control protocol for wireless sensor networks, the LMAC protocol. Our approach is to systematically investigate all possible con- nected topologies consisting of four and of five nodes. The analysis is performed by timed automaton model checking using Uppaal. The prop- erty of main interest is detecting and resolving collision. To evaluate this property for all connected topologies more than 8000 model checking runs were required. Increasing the number of nodes would not lead only to state space problem, but to much more extent cause an instance ex- plosion 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 ad- equacy of the protocol.

AB - In this paper we report about modelling and verification of a medium access control protocol for wireless sensor networks, the LMAC protocol. Our approach is to systematically investigate all possible con- nected topologies consisting of four and of five nodes. The analysis is performed by timed automaton model checking using Uppaal. The prop- erty of main interest is detecting and resolving collision. To evaluate this property for all connected topologies more than 8000 model checking runs were required. Increasing the number of nodes would not lead only to state space problem, but to much more extent cause an instance ex- plosion 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 ad- equacy of the protocol.

KW - METIS-242160

KW - CAES-PS: Pervasive Systems

KW - EWI-9447

KW - IR-66987

M3 - Report

T3 - CTIT Technical Report Series

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

PB - Distributed and Embedded Security (DIES)

CY - Enschede

ER -

Fehnker A, Fehnker A, van Hoesel LFW, Mader AH. Modelling and Verification of the LMAC Protocol for Wireless Sensor Networks. Enschede: Distributed and Embedded Security (DIES), 2007. 20 p. (CTIT Technical Report Series; TR-CTIT-07-09).