On the formal verification of the TCAS conflict resolution algorithms
- 22 November 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- Vol. 2 (01912216) , 1829-1834
- https://doi.org/10.1109/cdc.1997.657846
Abstract
TCAS (traffic alert and collision avoidance system) is an on-board protocol for detecting conflicts between aircraft and providing resolution advisories to the pilots. Because of its safety-critical role the TCAS software should ideally be "verified" before it can be deployed. The verification task is challenging, due to the complexity of the TCAS code and the hybrid nature of the system. We show how the essence of this very complicated problem can be captured by a relatively simple hybrid model, amenable to formal analysis. We then outline a methodology for establishing conditions under which the advisories issued by TCAS are safe.Keywords
This publication has 6 references indexed in Scilit:
- A verified hybrid controller for automated vehiclesPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Conflict resolution for multi-agent hybrid systemsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Verification of automated vehicle protection systemsPublished by Springer Nature ,1996
- A game-theoretic approach to hybrid system designPublished by Springer Nature ,1996
- Hybrid I/O automataPublished by Springer Nature ,1996
- The generalized railroad crossing: a case study in formal verification of real-time systemsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1994