Case study: Applying formal methods to the Traffic Alert and Collision Avoidance System (TCAS) II

Author

Britt, Joan J.

Author_Institution

Center for Adv. Aviation Syst. Dev., MITRE Corp., USA

fYear

1994

fDate

27 Jun-1 Jul 1994

Firstpage

39

Lastpage

51

Abstract

Requirements State Machine Language (RSML) evolved from statecharts during the development of the Traffic Alert and Collision Avoidance System (TCAS) II system requirements specification. This paper describes RSML and the TCAS II system requirements specification, which was reverse-engineered from pseudocode. This case study illustrates how formal methods have been applied to a safety-critical system, improving the assurance of safety in three areas: product review, process and personnel certification, and functional testing

Keywords

aerospace computing; aircraft instrumentation; formal specification; specification languages; RSML; Requirements State Machine Language; TCAS; TCAS II; Traffic Alert and Collision Avoidance System; aircraft onboard collision avoidance system; formal methods; functional testing; personnel certification; process certification; product review; reverse-engineered; safety assurance; safety-critical system; statecharts; system requirements specification; Air traffic control; Aircraft; Certification; Collision avoidance; Computer aided software engineering; Logic testing; Personnel; Product safety; Software safety; System testing;

fLanguage

English

Publisher

ieee

Conference_Titel

Computer Assurance, 1994. COMPASS '94 Safety, Reliability, Fault Tolerance, Concurrency and Real Time, Security. Proceedings of the Ninth Annual Conference on

Conference_Location

Gaithersburg, MD

Print_ISBN

0-7803-1855-2

Type

conf

DOI

10.1109/CMPASS.1994.318468

Filename

318468