Automated black-box testing with abstract VDM oracles

Abstract. In this paper the possibilities to automate black-box testing through formal requirement specifications are explored. More precisely, the formal method VDM (Vienna Development Method) serves to demonstrate that abstract requirement models can be used as test oracles for concrete software. The automation of the resulting testing frame-work is based on modern CASE-tools that support a light-weight approach to formal methods. The specification language used is VDM-SL, but the results are easily transferred into similar model oriented methods such as B, Z or RAISE.