This paper relates exeriences with formal methods that are relevant to the systems engineering activities of requirements specification, design documentation, and test case generation. Specificanlyu, this paper reviews the lessons learned from the application of formal methods to selected ocmponents of an air traffic management system. This project used experimental tools developed at the University of British OClumbia: S, a formal specificantion tool; HPP, an HTML documentation tool; and TCG, a test case generation tool. The components experimented on are from a recently fielded sytem 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 txt cases. This experience identified some ambiguities in the original specificantion, evaluated the feasibility of the experimental tools we used, and identified areas in which the tools could be improved.
展开▼
