Modelling and Verification of the LMAC Protocol for Wireless Sensor Networks

Share/Save/Bookmark

Fehnker, Ansgar and Hoesel van, Lodewijk and Mader, Angelika (2007) Modelling and Verification of the LMAC Protocol for Wireless Sensor Networks. [Report]

[img]
Preview
PDF
604Kb
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.
Item Type:Report
Faculty:
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/66987
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page

Metis ID: 242160