Formal Modeling and Verification of a Wireless Body Area Network (WBAN) Protocol: S-TDMA Protocol
Title | Formal Modeling and Verification of a Wireless Body Area Network (WBAN) Protocol: S-TDMA Protocol |
Publication Type | Conference Paper |
Year of Publication | 2017 |
Authors | Hamouda, R. Ben, Hafaiedh, I. Ben |
Conference Name | 2017 International Conference on Internet of Things, Embedded Systems and Communications (IINTEC) |
Keywords | access protocols, body area networks, body sensor networks, compositionality, Connectors, formal validation, formal verification, implanted devices, information processing systems, MAC protocol, MAC protocols, Media Access Protocol, Medium Access Control, Metrics, model checking, pubcrawl, real-time model checker, resilience, Resiliency, S-TDMA protocol, Scalability, scalable verification, TDMA, TDMA bus arbitration, temporal aspect modeling, time division multiple access, timed automata, WBAN, wearable devices, wireless body area network protocol, Wireless communication, Wireless sensor networks, WSN |
Abstract | WBANs integrate wearable and implanted devices with wireless communication and information processing systems to monitor the well-being of an individual. Various MAC (Medium Access Control) protocols with different objectives have been proposed for WBANs. The fact that any flaw in these critical systems may lead to the loss of one's life implies that testing and verifying MAC's protocols for such systems are on the higher level of importance. In this paper, we firstly propose a high-level formal and scalable model with timing aspects for a MAC protocol particularly designed for WBANs, named S-TDMA (Statistical frame based TDMA protocol). The protocol uses TDMA (Time Division Multiple Access) bus arbitration, which requires temporal aspect modeling. Secondly, we propose a formal validation of several relevant properties such as deadlock freedom, fairness and mutual exclusion of this protocol at a high level of abstraction. The protocol was modeled using a composition of timed automata components, and verification was performed using a real-time model checker. |
URL | https://ieeexplore.ieee.org/document/8325916 |
DOI | 10.1109/IINTEC.2017.8325916 |
Citation Key | hamouda_formal_2017 |
- time division multiple access
- resilience
- Resiliency
- S-TDMA protocol
- Scalability
- scalable verification
- TDMA
- TDMA bus arbitration
- temporal aspect modeling
- real-time model checker
- timed automata
- WBAN
- Wearable devices
- wireless body area network protocol
- Wireless communication
- wireless sensor networks
- WSN
- access protocols
- pubcrawl
- model checking
- Metrics
- Medium Access Control
- Media Access Protocol
- MAC protocols
- MAC protocol
- information processing systems
- implanted devices
- formal verification
- formal validation
- Connectors
- Compositionality
- body sensor networks
- body area networks