Automating the Generation of Test Cases from Object-Z Specifications

In this paper, we propose a test case generation technique based on Object-Z specification of a class, based on formalization of the test case generation strategy. The proposed technique enables automatic generation of test cases from an Object-Z specification, under the specified strategy. We also propose to enhance the prototype tool TinMan, which was originally developed to automate derivation and management of testing information for specification-based class testing, by introducing semantics knowledge for the application of test case generation strategies in a format acceptable to the tool