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.

Document type: Part of book or chapter of book

Full document

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