Biblio

This paper presents a framework for medium access control (MAC) and physical (PRY) cross-layer security design of wireless avionics intra-communications (WAICs). The paper explores the different options based on the latest results of MAC-PRY cross-layer design and the available standard technologies for WAICs. Particular emphasis is given to solutions based on multiple-input multiple-output (MIMO) systems and recent developments towards a wireless technology with ultra-low latency and high reliability in the context of 5G and machine-type traffic support. One major objective is to improve WAICs technology and thus match the real-time, reliability and safety critical performance of the internal aeronautics bus technologies (e.g., ARINC 664). The main identified vulnerabilities and potential solutions are explored, as well as their impact on system design complexity and feasibility for wireless networks on-board aircraft. The solutions are presented in the context of the European project SCOTT (secure connected trustable things) using the recently released reference architecture for trusted IoT systems. Other aspects of SCOTT such as trust, privacy, security classes, and safety are also discussed here for the aeronautics domain.

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.