Modelling and Verification of the LMAC Protocol for Wireless Sensor Networks

Fehnker, Ansgar and Hoesel van, Lodewijk and Mader, Angelika (2007) Modelling and Verification of the LMAC Protocol for Wireless Sensor Networks. In: 6th International Conference on Integrated Formal Methods, IFM 2007, 2-5 July 2007, Oxford, Britain.

PDF
Restricted to UT campus only: Request a copy
249Kb

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.
Item Type:	Conference or Workshop Item
Copyright:	© 2007 Springer
Faculty:	Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:	Robotics and Mechatronics (CE)
Link to this item:	http://purl.utwente.nl/publications/62160
Official URL:	http://dx.doi.org/10.1007/978-3-540-73210-5_14
Export this item as:	BibTeX EndNote HTML Citation Reference Manager

Show download statistics for this publication

Repository Staff Only: item control page

Metis ID: 246008