From Object-Z specifications to ClassBench test suites

This paper describes a method for specification-based class testing that in corporates test case generation, execution, and evaluation based on formal specifications. This work builds on previous achievements in the areas of s pecification-based testing and class testing by integrating the two within a single framework, The initial step of the method is to generate test temp lates for individual operations from a specification written in the Object- Z specification language, These test templates are combined to produce a fi nite state machine for the class that is used as the basis for test case ex ecution using the ClassBench test execution framework. An oracle derived fr om the Object-Z specification is used to evaluate the outputs. The method i s explained using a simple example and its application to a more substantia l case study is also discussed Copyright (C) 2000 John Whey & Sons, Ltd.