Using {log} as a test case generator for Z specifications

CRISTIÁ, MAXIMILIANO; ROSSI, GIANFRANCO

Catania

Congreso; 28-esimo Convegno Italiano di Logica Computazionale; 2013

Gruppo Ricercatori e Utenti Logic Programming

The Test Template Framework (TTF) is a model-based testing method for the Z notation, a formal specification language based on first-order logic and set theory. In the TTF, test cases are generated from test specifications, which are predicates written in Z. In this paper we show how {log} can be applied as a test case generator for the TTF. {log} is a Constraint Logic Programming language that embodies thefundamental forms of set designation and a number of primitive operations for set management. As such, it can find solutions of first-order logic formulas involving set-theoretic operators. According to our experiments, {log} produces promising results as concerns the effectiveness and efficiency in finding solutions (i.e. test cases) out of a number of non-trivial test specifications.