Practical
Experience Applying Formal Methods to Air Traffic Management Software.
by Richard Yates, James
Andrews and Phil Gray
| |
Practical
Experience Applying Formal Methods to Air Traffic Management Software.
by Richard Yates, James
Andrews and Phil Gray
|
| formalWARE
project
formalWARE
formalWARE
|
Abstract
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.
Download Postscript
To be presented at INCOSE '98: International Council on Systems Engineering, July 1998, Vancouver B.C., Canada
|
