Formal Specification of a Voice Communication System used in Air Traffic Control

Despite the fact that research interest in formal methods has been growing rapidly in the last years, they are rarely used in industry. The company FREQUENTIS has identified that formal methods may be helpful to improve its products. The aim of this thesis is to introduce the idea of formal methods to the company FREQUENTIS. So-called light-weight formal methods have been used to allow a smooth integration of formal methods into their current development process. To show different applications of formal methods, three different tasks have been performed. This thesis describes these tasks along with their results. The whole work is based on the VCS 3020S voice communication system, which is intended for voice communication in air traffic control. First of all, an explicit formal specification of a safety critical part of the system has been created. VDM ++ has been used as formal specification language. During the specification numerous open issues have been identified. These issues a..