Formal specification techniques as a catalyst in validation

The American Heritage Dictionary defines a catalyst as a substance, usually present in small amounts relative to the reactants, that modifies and especially increases the rate of a chemical reaction without being consumed in the process. This article reports on the experience gained in an industrial project that formal specification techniques form such a catalyst in the validation of complex systems. These formal development methods improve the validation process significantly by generating precise questions about the system´s intended functionality very early and by uncovering ambiguities and faults in textual requirement documents. This project has been a cooperation between the IST and the company Frequentis. The Vienna Development Method (VDM) has been used for validating the functional requirements and the existing acceptance tests of a network node for voice communication in air traffic control. In addition to several detected requirement faults, the formal specification highlighted how additional test-cases could be derived systematically