School of Computing

Testing refinements by refining tests

J. Derrick and E. A. Boiten

In J. P. Bowen, A. Fett, and M. G. Hinchey, editors, ZUM'98: The Z Formal Specification Notation, volume 1493 of Lecture Notes in Computer Science, pages 182-196. Springer-Verlag, September 1998.


One of the potential benefits of formal methods is that they offer the possibility of reducing the costs of testing. A specification acts as both the benchmark against which any implementation is tested, and also as the means by which tests are generated. There has therefore been interest in developing test generation techniques from formal specifications, and a number of different methods have been derived for state based languages such as Z, B and VDM. However, in addition to deriving tests from a formal specification, we might wish to refine the specification further before its implementation.

The purpose of this paper is to explore the relationship between testing and refinement. As our model for test generation we use a DNF partition analysis for operations written in Z, which produces a number of disjoint test cases for each operation. In this paper we discuss how the partition analysis of an operation alters upon refinement, and we develop techniques that allow us to refine abstract tests in order to generate test cases for a refinement. To do so we use (and extend existing) methods for calculating the weakest data refinement of a specification.

Download publication 210 kbytes (PostScript)

Bibtex Record

author = {J. Derrick and E. A. Boiten},
title = {Testing Refinements by Refining Tests},
month = {September},
year = {1998},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {},
    ISBN = {3 540 65070 9},
    booktitle = {ZUM'98: The Z Formal Specification Notation},
    editor = {J. P. Bowen and A. Fett and M. G. Hinchey},
    publisher = {Springer-Verlag},
    series = {Lecture Notes in Computer Science},
    volume = {1493},

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014