Formal specification of a voice communication system used in air traffic control an industrial application of light-weight formal methods using vdm

Abstract

A joint project of the Austrian company Frequentis1 and the Technical University Graz demonstrates the applicability of executable formal models2. The formal method VDM++ has been applied to specify a safety critical voice communication system (VCS) for air-traffic control. Besides the expected improvement of the informal speciffication documents, 64 defects have been found, the efficiency of the system test-cases to cover the functionality of the VCS has been analyzed. In order to get a test-coverage measure, the formal specification has been animated with existing system test-cases using IFAD’s VDMTools.

Original document

The different versions of the original document can be found in:

• https://link.springer.com/content/pdf/10.1007%2F3-540-48118-4_59.pdf

• http://link.springer.com/content/pdf/10.1007/3-540-48118-4_59,

http://dx.doi.org/10.1007/3-540-48118-4_59

• https://link.springer.com/chapter/10.1007%2F3-540-48118-4_59,

http://core.ac.uk/display/24280658,

https://www.scipedia.com/public/Horl_Aichernig_2007a,

https://academic.microsoft.com/#/detail/154294185

• [ ]