A test oracle provides a means for determining whether an implementation behaves according to its specification. A passive test oracle checks that the correct behaviour has been implemented, but does not implement the behaviour itself. In previous work, we have presented a method that allows us to derive passive C++ test oracles from formal specifications written in Object-Z. We describe the "Warlock" prototype tool that supports the method. Warlock is built on top of an existing Object-Z type checker and generates oracle code for a substantial subset of the Object-Z language. We describe the architecture of Warlock and its application to a number of Object-Z specifications. We also discuss its current limitations.

This paper reports on an industrial pilot project that introduces systematic, automated module testing for embedded software in distributed, real-time, control systems. The systems are used in safety-related applications, are complex in nature, and hence have strong requirements for test coverage, auditability and repeatability. This paper explores issues of isolating modules from the run-time environment, improving integration of testing into the development environment, automating testing, and improving test planning and documentation. Metrics were gathered throughout the project that allow a coarse cost-benefit evaluation. Code coverage metrics for statement and branch coverage were also gathered using a commercial code coverage analysis tool. The testing exposed a number of latent faults within the software, and the overall results of the project show that module testing is feasible for this complex, embedded software.

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

In this paper, we present an approach that combines specification-based testing and class testing. In particular, we provide a method for generating Finite State Machines (FSMs) from formal, object-oriented specifications, and use the ClassBench testing framework to build a test suite from those formally generated FSMs. We briefly outline our approach and focus on one step in the approach; the transformation of the formally derived FSM into a ClassBench testgraph, which is used by ClassBench to drive the test execution. We illustrate the method with a simple bounded queue class, and discuss the application of the method to a larger example, which is a simplified model of a process scheduling system.

A test oracle provides a means for determining whether an implementation functions according to its specification. A passive test oracle checks the behaviour of the implementation, but does not attempt to reproduce this behaviour. The paper describes the translation of formal specifications of container classes to passive test oracles. Specifically, we use Object-Z for specifications and C++ for oracles. We discuss several practical issues for the use of formal specifications in test oracle generation. We then present the translation process and illustrate it with an example based on an integer set class. Our approach is illustrated with an example based on an integer set class.

We describe part of an STL conformance test suite under development. Test suites for all of the STL containers have been written, demonstrating the feasibility of thorough and highly automated testing of industrial component libraries. We describe affordable test suites that provide good code and boundary value coverage, including the thousands of cases that naturally occur from combinations of boundary values. We show how two simple oracles can provide fully automated output checking for all the containers. We refine the traditional categories of black-box and white-box testing to specification-based, implementation-based and implementation-dependent testing, and show how these three categories highlight the key cost/thoroughness trade-offs.

This paper describes the translation of Object-Z specifications of container classes to C++ test oracle classes. It presents a three-stage translation process and describes how the derived test oracles are integrated into the ClassBench testing framework. The method caters for object-oriented features such as inheritance and aggregation. Translation issues and the limitations of the method are discussed. Our approach is illustrated with an example based on an integer set class.