Premium
3.3.4 Practical Experience Applying Formal Methods to Air Traffic Management Software
Author(s) -
Yates Richard,
Andrews Jamie,
Gray Phil
Publication year - 1998
Publication title -
incose international symposium
Language(s) - English
Resource type - Journals
ISSN - 2334-5837
DOI - 10.1002/j.2334-5837.1998.tb00055.x
Subject(s) - documentation , computer science , formal methods , software engineering , formal specification , air traffic control , systems engineering , test (biology) , engineering management , engineering , programming language , paleontology , biology , aerospace engineering
This paper relates experiences with formal methods that are relevant to the systems engineering activities of requirements specification, design documentation, and test case generation. Specifically, this paper reviews the lessons learned from the application of formal methods to selected components of an air traffic management system. This project used experimental tools developed at the University of British Columbia: S, a formal specification tool; HPP, an HTML documentation tool; and TCG, a test case generation tool. The components experimented on are from a recently fielded system written in C++ using unimplemented pre‐ and post‐conditions on components. The purpose of the experiment was to evaluate the usefulness of these formal methods to uncover design or logic errors in the system components and to assist in designing test cases. This experience identified some ambiguities in the original specification, evaluated the feasibility of the experimental tools we used, and identified areas in which the tools could be improved.