Pruning Testing Trees in the Test Template Framework by Detecting Mathematical Contradictions

Fastest is an automatic implementation of Phil Stocks and David Carrington´s Test Template Framework (TTF), a model-based testing (MBT) framework for the Z formal notation. In this paper we present a new feature of Fastest that helps TTF users to eliminate inconsistent test classes automatically. The method is very simple and practical, and makes use of the peculiarities of the TTF. Perhaps its most interesting features are extensibility and ease of use, since it does not assume previous knowledge on theorem proving. Also we compare the solution with a first attempt using the Z/EVES proof assistant and with the HOL-Z environment. At the end, we show the results of an empirical assessment based on applying Fastest to four real-world, industrial-strength case studies and to six toy examples.