Issue No. 03 - May/June (2000 vol. 17)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/52.896246
To show that lightweight approaches can facilitate the technological transfer of formal development methods, the authors report on their experiences using VDM++ to specify a safety-critical air traffic control voice communication system. Their approach raised both the quality of the informal system specification as well as the efficiency of the system test suites they used.
B. K. Aichernig and J. Hörl, "Validating Voice Communication Requirements Using Lightweight Formal Methods," in IEEE Software, vol. 17, no. , pp. 21-27, 2000.