Modelling and Verification of the LMAC Protocol for Wireless Sensor Networks
| Autor: | Fehnker, Ansgar, van Hoesel, Lodewijk, Mader, Angelika H., Davis, Jim, Gibbons, Jeremy |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2007 |
| Předmět: |
Model checking
CR-F.3.1 Computer science business.industry Real-time computing Timed automaton 020206 networking & telecommunications Access control 02 engineering and technology Network topology Collision CAES-PS: Pervasive Systems 0202 electrical engineering electronic engineering information engineering Computer Science::Networking and Internet Architecture State space 020201 artificial intelligence & image processing business Protocol (object-oriented programming) Wireless sensor network Computer network |
| Zdroj: | Integrated Formal Methods: 6th International Conference, IFM 2007, Oxford, UK, July 2-5, 2007. Proceedings, 253-272 STARTPAGE=253;ENDPAGE=272;TITLE=Integrated Formal Methods Lecture Notes in Computer Science ISBN: 9783540732099 IFM |
| ISSN: | 0302-9743 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|