DocumentCode :
1387290
Title :
High-level modeling and analysis of the traffic alert and collision avoidance system (TCAS)
Author :
Livadas, Carolos ; Lygeros, John ; Lynch, Nancy A.
Author_Institution :
Lab. for Comput. Sci., MIT, Cambridge, MA, USA
Volume :
88
Issue :
7
fYear :
2000
fDate :
7/1/2000 12:00:00 AM
Firstpage :
926
Lastpage :
948
Abstract :
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); 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, which are amenable to format 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 the 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.
Keywords :
air traffic control; automata theory; avionics; closed loop systems; collision avoidance; safety-critical software; aircraft collision threats; avionics system; closed-loop system behavior; complex safety-critical systems; core components; format analysis; high-level analysis; high-level modeling; high-level verification techniques; hybrid I/O automata; traffic alert and collision avoidance system; Aerospace electronics; Air traffic control; Aircraft; Airplanes; Collision avoidance; Road accidents; Software testing; System software; System testing; Traffic control;
fLanguage :
English
Journal_Title :
Proceedings of the IEEE
Publisher :
ieee
ISSN :
0018-9219
Type :
jour
DOI :
10.1109/5.871302
Filename :
871302
Link To Document :
بازگشت