From Object-Z specifications to ClassBench test suites
David B. Carrington, Ian MacColl, Jason McDonald, Leesa Murray, Paul A. Strooper · Software Testing Verification and Reliability · 2000
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. Keywords: specification-based testing, Object-Z, class testing, ClassBench, oracles 1