Automatically Generating Information from a Z Specification to Support the Classification Tree Method

摘要

The Classification Tree Method provides a flexible basis for systematic testing. Traditionally the generation of a classification tree has been entirely manual. This paper introduces a new approach that extracts predicates from the Z specification of an operation and builds a Classification Tree from these predicates. It thus shows how the generation of a Classification Tree may be semi-automated on the basis of a Z specification. The paper also defines the notion of the test context of a predicate that determines when the value of this predicate is relevant. The test context is used to reduce the number of tests produced from the Classification Tree.