High-Level Modeling and Analysis of the Traffic Alert and Collision Avoidance System (TCAS)

In this paper, we demonstrate a high-level approach to modeling, analyzing, and verifying complex safety-critical systems through a case study on the Traffic Alert and Collision Avoidance System (TCAS) [1--3]; an avionics system that detects and resolves aircraft collision threats. Due to the complexity of the TCAS software and the hybrid nature of the closed-loop system, the traditional testing technique of exhaustive simulation does not constitute a viable verification approach. Moreover, the detailed specification of the system software employed to date as a means towards analysis and verification, neither help in intuitively understanding the behavior of the system, nor enable the analysis of the closed-loop system behavior. We advocate defining high-level hybrid system models that capture the behavior not only of the software, but also of the airplanes, sensors, pilots, etc. In particular, we show how the core components of TCAS can be captured by relatively simple Hybrid I/O Automata (HIOA) [4, 5], which are amenable to formal analysis. We then outline a methodology for establishing conditions under which TCAS guarantees sufficient separation in altitude for aircraft involved in collision threats. The contributions of this paper are the high-level models of the closed-loop TCAS system and the demonstration of the usefulness of high-level modeling, analysis, and verification techniques