Testing Renements of State-based Formal Specications

A specication provides a concise description of a system, and can be used as both the benchmark against which any implementation is tested, and also as a means to generate tests. Formal specications have potential advantages over informal descriptions because they oer the possibility of reducing the costs of testing by automating part of the testing process. This observation has led to considerable interest in developing test generation techniques from formal specications, and a number of dierent methods have been derived for state based formalisms such as Z, B and VDM. However, after tests have been derived from a formal specication, the specication might be rened further before its implementation, and therefore a mechanism is needed to relate the abstract tests to the rened implementation. The purpose of this paper is to provide such a method by exploring the relationship between testing and renement. In this paper a model for test generation is used which constructs a nite state machine (FSM) from a Z specication by using a DNF partition analysis of the state and operations. The nite state machine is then used to derive suitable FSM together with the information about the renement embodied in the retrieve relation. This means that it is possible to test an implementation by generating a new concrete nite state machine from a set of abstract tests