Formal Specification of a Voice Communication System used in Air Traffic Control - An Industrial Application of Light-weight Formal Methods using VDM++

: During the last few years light-weight approaches to formal development methods have been proposed in order to facilitate the technological transfer of these techniques. This article presents the results and experiences gained in an industrial project, in which VDM ++ has been applied to specify a safety critical voice communication system for air-traffic control. It is shown that an executable VDM ++ model can be used to raise both, the level of quality of the informal system specification, as well as the efficiency of existing system test-suites. Furthermore, a selected change request serves to demonstrate how maintenance is supported by a formal model. For all the tasks in the project, precise time-effort figures are presented. 1 Introduction During the last few years the interest in formal software development has been growing rapidly. Several reasons can be identified: The availability of commercial tools to support the developer, the integration with informal approaches, a..