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 partition.

While the DNF approach has many advantages, it may lead to a combinatorial explosion. We have approached this problem in two ways.

Back to Rob Hierons' home page

Last updated: 11th August 2004.

Disclaimer The contents of this page falls outside the responsibility of Brunel University.