Note: This content is accessible to all versions of every browser. However, this browser does not seem to support current Web standards, preventing the display of our site's design details.


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


C. Livadas, J. Lygeros, N: Lynch

Proceedings of IEEE, vol. 88, pp. 926-948

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 toward analysis and verification neither helps in intuitively understanding the behavior of the system nor enables 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 [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.


Type of Publication:


File Download:

Request a copy of this publication.
(Uses JavaScript)
% Autogenerated BibTeX entry
@Article { LivLyg:2000:IFA_2544,
    author={C. Livadas and J. Lygeros and N: Lynch},
    title={{High-Level Modeling and Analysis of the Traffic Alert and
	  Collision Avoidance System (TCAS)}},
    journal={Proceedings of IEEE},
Permanent link