Testing from a Z specification
Languages such as Z, VDM, and B specify an operation from a system
by using predicate logic to state how the input and state before
the operation relates to the output and the state after the operation.
A number of authors have considered the problem of automating test
generation on the basis of a specification written in such a language.
One of the earliest, and most important, approaches to test
automation is the DNF method. Here the
specification is rewritten to Disjunctive Normal Form and a
partition of the input domain is formed from the preconditions of
the disjuncts. Test cases are drawn from each subdomain of the
While the DNF approach has many advantages, it may lead to a
combinatorial explosion. We have approached this problem
in two ways.
Only transform the specification part of the way to DNF.
This approach is inspired by the observation that the transformation
to DNF can be more fine grained than is required and thus
can expand the specification further than is required.
In addition, by only transforming the specification as
far as required we reduce the potential for unwanted
redundancy in our test suite.
Produce a classification tree from the specification and
combine classes from this tree to form
abstract test cases. While the use of all
combinations of classes might reproduce the combinatorial
explosion found in the DNF approach, the tester can choose to use
only some of the combinations.
R.M. Hierons, M. Harman, and H. Singh, 2003,
Automatically generating information from a Z specification to support the Classification Tree Method,
3rd International Conference of B and Z Users,
June 4-6, 2003, LNCS volume 2651, pages 388-407.
R. M. Hierons, S. Sadeghipour, and H. Singh, 2001,
Testing a System
specified using Statecharts and Z,
Information and Software Technology,
43 2, pp. 137-149.
R.M. Hierons, 1997,
Testing from a Z specification,
The Journal of Software Testing, Verification, and Reliability,
7 1, pp. 19-33.
Back to Rob Hierons'
Last updated: 11th August 2004.
Disclaimer The contents of this page falls
outside the responsibility of Brunel University.