Pruning Testing Trees by Automatic Theorem Proving

CRISTIÁ, MAXIMILIANO; ALBERTENGO, PABLO; RODRÍGUEZ MONETTI, PABLO

2009-02-02/2010-03-01

1-16

Informática (software)

Varios campos

Fastest is the first tool giving 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 prune testing trees automatically. The technique is based on a sort of automatic theorem proving that makes use of the peculiarities of the TTF. Also we compare the solution with a first attempt using the Z/EVES proof assistant. At the end, we show the results of an empirical assessment based on applying our approach to two real-world, industrial-strength case studies and to six toy examples.