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

The PDF file did not load properly or your web browser does not support viewing PDF files. Download directly to your device: Download PDF document

Original document

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

Back to Top

Document information

Published on 01/01/2007

Volume 2007, 2007
DOI: 10.1007/3-540-48118-4_59
Licence: CC BY-NC-SA license

Document Score


Views 0
Recommendations 0

Share this document

claim authorship

Are you one of the authors of this document?