Carolos Livadas, John Lygeros, and Nancy A. Lynch. High-Level Modeling and Analysis of TCAS. Proceedings of IEEE, Special Issue on Hybrid Systems: Theory & Applications, Vol. 88, No. 7, July 2000.
[postscript, pdf, bib]

Abstract

In this paper, we demonstrate a high-level approach to modeling and analyzing complex safety-critical systems through a case study in the area of air traffic management. In particular, we focus our attention on the Traffic Alert and Collision Avoidance System (TCAS); an on-board conflict detection and resolution system which alerts pilots to the presence of nearby aircraft that pose a mid-air collision threat and issues conflict resolution advisories. Due to the complexity of the TCAS software and the hybrid nature of the closed-loop system, the traditional testing techniques through simulation do not constitute a viable verification approach. Moreover, the formal analysis techniques applied to air traffic management systems, which primarily involve the detailed specification of the system software, neither help in intuitively understanding the behavior of the system, nor enable the analysis of the closed-loop system behavior. To aid people in analyzing and designing such systems, we advocate defining high-level mathematical system models that capture the behavior not only of the software, but also of the airplanes, sensors, and pilots---that is, high-level hybrid system models. In particular, we show how the core components of the TCAS system can be captured by relatively simple Hybrid I/O Automata (HIOA), which are amenable to formal analysis. We then outline a methodology for establishing conditions under which the conflict resolution advisories issued by TCAS guarantee sufficient separation in altitude for aircraft involved in mid-air collision threats. The contributions of this paper are the high-level models of the TCAS system, which may be used as a basis for studying a wide range of TCAS properties, and the demonstration of the potential usefulness and practicality of high-level modeling and analysis techniques.