From Object-Z specifications to ClassBench test suites
This paper describes a method for specification-based class testing that incorporates test case generation, execution, and evaluation based on formal specifications. This work builds on previous achievements in the areas of specification-based testing and class testing by integrating the two within a single framework, The initial step of the method is to generate test templates for individual operations from a specification written in the Object-Z specification language, These test templates are combined to produce a finite state machine for the class that is used as the basis for test case execution using the ClassBench test execution framework. An oracle derived from the Object-Z specification is used to evaluate the outputs. The method is explained using a simple example and its application to a more substantial case study is also discussed Copyright (C) 2000 John Whey & Sons, Ltd.
object-z classbench class testing specification-based testing oracles