Requirements Engineering, IEEE International Conference on (2000)
June 19, 2000 to June 23, 2000
Johann Hörl , Technical University Graz
Bernhard K. Aichernig , Technical University Graz
During the last, few years' lightweight approaches to formal development methods have been proposed in order to facilitate the technological transfer of formal methods. “Lightweight” means that a precise and unambiguous formal specification language is used in order to raise the quality of a system's description, without focusing on proofs . This article presents the results and experiences gained in an industrial project where VDM ++ , an object oriented extension of the Vienna Development Method, has been applied in such a lightweight manner. In the joint project of the Austrian company Frequent is and the Technical University Graz , a safety critical voice communication system (VCS) for air-traffic control has been specified and validated. It serves as the sole communication system between the pilots, the air-traffic control personnel at the tower, the ground personnel on the runways, other parties external to the airport and even other airports. During the formal specification of the VCS system a total number of 64 ambiguous, contradictory or incomplete issues have been detected in the various documents of the system. These issues have been summarized in a catalogue of questions. All of them have been resolved, supported by system experts.
J. Hörl and B. K. Aichernig, "Requirements Validation of a Voice Communication System Used in Air Traffic Control," Requirements Engineering, IEEE International Conference on(ICRE), Schaumburg, Illinois, 2000, pp. 190.