On the formal verification of the TCAS conflict resolution algorithms

Author

Lygeros, John ; Lynch, Nancy

Author_Institution

Lab. for Comput. Sci., MIT, Cambridge, MA, USA

Volume

2

fYear

1997

fDate

10-12 Dec 1997

Firstpage

1829

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

aircraft control; automata theory; computerised monitoring; formal verification; protocols; safety-critical software; TCAS; conflict resolution algorithms; conflicts detection; formal analysis; formal verification; hybrid model; on-board protocol; resolution advisories; safety-critical role; traffic alert and collision avoidance system; Air traffic control; Aircraft; Algorithm design and analysis; Collision avoidance; Computer science; Formal verification; Laboratories; Protocols; Software safety; Traffic control;

fLanguage

English

Publisher

ieee

Conference_Titel

Decision and Control, 1997., Proceedings of the 36th IEEE Conference on

Conference_Location

San Diego, CA

ISSN

0191-2216

Print_ISBN

0-7803-4187-2

Type

conf

DOI

10.1109/CDC.1997.657846

Filename

657846