Formal Verification of the TCAS Algorithms John Lygeros, Carl Livadas, and Nancy Lynch

The Traffic Alert and Collision Avoidance System (TCAS) is an on-board conflict detection and resolution algorithm for commercial aircraft. Its task is to monitor air traffic in the vicinity of the aircraft and provide the pilot with information on neighboring aircraft that may pose a threat and advisories on how to resolve the conflicts. The algorithm processes data from sensor and communication devices and uses a rather complicated protocol to decide when aircraft are in conflict and what maneuvers the pilots should perform to resolve it. In view of its complexity, the TCAS software needs to be verified before it can be deployed. The software was developed through a sequence of progressive refinements, starting with abstract, high level specifications that get refined down to pseudo-code and regular computer code. Part of the verification problem involves proving that each level in this process implements the higher level specifications. Our work focuses on a different problem: investigating the performance of the closed loop system formed when the proposed algorithm is coupled with the aircraft dynamics. So far the primary verification technique used in this context has been simulation. Successful results in extensive simulations provide a certain level of confidence in the algorithm. More importantly, unsuccessful simulation runs pinpoint situations where the performance of the algorithm is insufficient and often suggest modifications to improve it. In safety critical situations (like the ones that TCAS is called upon to resolve) a ``certain level of confidence'' in the algorithm may be insufficient. Moreover, repeated changes in the algorithm itself, partly in response to unsuccessful simulation runs, make the verification by simulation process very inefficient, as a large number of simulations may have to be re-executed even for small changes. These observations suggest the need for a more formal verification process, one that not only will provide absolute confidence in the algorithm (under a set of assumptions) but may also be easily modified if slight changes are made to the system (for example thresholds or model parameters are changed). In this project we are developing such formal verification approach. The overall TCAS system is hybrid, involving both continuous and discrete dynamics; the former arise from the aircraft, sensors and pilot reaction and the latter from the thresholds and discrete message passing used by the TCAS algorithm. Therefore any verification effort will have to involve hybrid techniques. Our work makes use of a combination of techniques from control theory (traditionally associated with continuous systems) and distributed algorithms (traditionally associated with discrete systems) to tackle the verification problem. We seek to prove safety theorems, in particular that (under certain assumptions) the proposed TCAS algorithm guarantees an adequate level of minimum separation between the aircraft. Related Publications John Lygeros and Nancy Lynch. On the Formal Verification of the TCAS Conflict Resolution Algorithms. Proceedings of the 36th IEEE Conference on Decision and Control, San Diego, CA, December 1997. Abstract / .pdf Carolos Livadas, John Lygeros, 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. Abstract / .pdf Carolos Livadas, John Lygeros, and Nancy A. Lynch. High-Level Modeling and Analysis of TCAS. Proceedings of the IEEE, Special Issue on Hybrid Systems: Theory & Applications, volume 88, number 7, July 2000..pdf Abstract

TOC / LCS / MIT Last modified: Fri Jan 16 10:28:24 1998	Comments?