Test case design based on Z and the classification-tree method

Software testing often consumes up to 50 percent of the overall software costs. A large amount of time and money within the test process is spent due to incomplete, inconsistent or ambiguous informal specifications of the test objects. A more formal approach to the early phases of software development can reduce the error rate drastically and in addition, can significantly improve the central testing activities like test case design and test evaluation. This paper presents an approach for generating test cases from formal specifications written in Z by combining the classification-tree method for partition testing with the disjunctive normal form approach. Firstly, a classification tree describing high level test cases is constructed from the formal specification of the test object. Then the high level test cases are further refined by generating a disjunctive normal form for them. The refined test cases obtained this way cover all specified aspects of the system explicitly and also contain all information necessary to evaluate the test results. The proposed combination of the classification-tree method with the disjunctive normal form approach preserves advantages of both methods, overcomes most of their limitations, and can be supported by tools.