A novel way to design ADS-B using UML and TLA+ with security as a focus

Abstract

Automatic Dependent Surveillance-Broadcast (ADS-B) is the future of aviation. It is a vast system that provides situational awareness for the aviator and regulator at a very low cost and does so with the aid of multiple disparate systems working closely together and communicating with one another. ADS-B uses the Global Navigation Satellite System (GNSS/ GPS) to locate elements. Weather information and ground-based information is also transmitted wirelessly. The system is designed to be open, unencrypted, and accessible to actors throughout the world. However, this leaves it open to attacks. The use of GNSS and other wireless technologies also carries over their security vulnerabilities into ADS-B. Certain issues have arisen due to both component-system failures and malicious attacks. Most obvious solutions impinge on the openness and transparency of the system. Past research has indicated that security must be built into a system design itself and cannot be retrofitted. We want to showcase such a design process for ADS-B. Our pathway to do so is to first create Universal Modeling Language (UML) diagrams to showcase security and safety issues and responses. These UML diagrams will then help us to model state and sequence diagrams. These will then be used to create a TLA+ model of one selected security methodology. We then run the TLC model checking on it to find loopholes and plug gaps in our scheme. We managed to create such models and prove deadlock-free running using only software tools. Our eventual goal is to develop a comprehensive formal specification for ADS-B model-creation and checking.