Title :
Case study: Applying formal methods to the Traffic Alert and Collision Avoidance System (TCAS) II
Author_Institution :
Center for Adv. Aviation Syst. Dev., MITRE Corp., USA
fDate :
27 Jun-1 Jul 1994
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;
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
DOI :
10.1109/CMPASS.1994.318468
