Biblio

Tactical Data Link (TDL) is one of the important elements in Network Centric Warfare (NCW). TDL provides the means for rapid exchange of tactical information between air, ground, sea units and command centers. In military operations, TDL has high demands for resilience, responsiveness, reliability, availability and security. MANET has characteristics that are suitable for the combat environment, namely the ability to self-form and self-healing so that this network may be applied to the TDL system. To produce high performance in MANET adapted for TDL system, an efficient MAC Protocol method is needed. This paper provides a survey of several MAC Protocol methods on a tactical MANET. In this paper also suggests some improvements to the MANET MAC protocol to improve TDL system performance.

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.