Carolos Livadas, John Lygeros, and Nancy A. Lynch. High-Level Modeling and Analysis of TCAS. Proceedings of the 20th IEEE Real-Time Systems Symposium (RTSS'99), Phoenix, Arizona, pages 115-125, December, 1999.
[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. 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 this complex 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. Although our results are intended only as illustrations of high-level modeling and analysis techniques, the TCAS system models provide a foundation for study of a wide range of properties of the system's behavior.