Biblio

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.

This paper proposes a novel wireless MAC-layer approach towards achieving channel access anonymity. Nodes autonomously select periodic TDMA-like time-slots for channel access by employing a novel channel sensing strategy, and they do so without explicitly sharing any identity information with other nodes in the network. An add-on hardware module for the proposed channel sensing has been developed and the proposed protocol has been implemented in Tinyos-2.x. Extensive evaluation has been done on a test-bed consisting of Mica2 hardware, where we have studied the protocol's functionality and convergence characteristics. The functionality results collected at a sniffer node using RSSI traces validate the syntax and semantics of the protocol. Experimentally evaluated convergence characteristics from the Tinyos test-bed were also found to be satisfactory.