Options
Formal analysis and verification of the IEEE 802.15.4 DSME slot allocation
Publikationstyp
Conference Paper
Date Issued
2016-11-13
Sprache
English
Institut
TORE-URI
Start Page
140
End Page
147
Citation
MSWiM 2016 - Proceedings of the 19th ACM International Conference on Modeling, Analysis and Simulation of Wireless and Mobile Systems: 140-147 (2016-11-13)
Publisher DOI
Scopus ID
Providing dependability is still a major issue for wireless mesh networks, which restrains their application in industrial contexts. The widespread CSMA/CA medium access can provide high throughput and low latency, but can not prevent packet loss due to collisions, especially in very large and dense networks. Time slotted medium access techniques together with a distributed slot management, as proposed by the Distributed Synchronous Multi-channel Extension (DSME) of the IEEE 802.15.4 standard, are promising to provide low packet loss, high scalability and bounded end-to-end delays. However, our implementation, openDSME, exposed some weaknesses. While the allocated slots allow for reliable data transmission, the slot management itself is conducted via CSMA/CA and is thus vulnerable to packet loss, eventually leading to an inconsistent slot allocation. This paper uses the UPPAAL framework for formal analysis and verification of the slot management process. The analysis identifies weaknesses of the slot allocation process under communication and node failures. However, it is shown that inconsistencies are eventually resolved and improvements to the procedure are proposed that reduce the negative impact of failed slot allocation procedures significantly.
DDC Class
004: Informatik
More Funding Information
Supported by the German Federal Ministry for Economic Affairs and Energy (BMWi) in the AutoR project (0325629D).