A rigorous method for test templates generation from object-oriented specifications

摘要

This paper describes a rigorous method that investigates the suitability of formal specifications written in Object-Z specification language for testing object-oriented software implementation in a black-box fashion. The insight gained in the formalization of a model, the inherent abstractions, and formally specified intended behaviours and exceptions lead to the generation of test templates that are free from any implementation bias. The method described in this paper is an extension of the one proposed by Stocks and Carrington.