{log} as a test case generator for the test template framework

Abstract

{log} (pronounced 'setlog') is a Constraint Logic Programming language that embodies the fundamental 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. The Test Template Framework (TTF) is a model-based testing method for the Z notation. In the TTF, test cases are generated from test specifications, which are predicates written in Z. In turn, the Z notation is based on first-order logic and set theory. In this paper we show how {log} can be applied as a test case generator for the TTF. According to our experiments, {log} produces promising results compared to other powerful constraint solvers supporting the Z notation, such as ProB. © 2013 Springer-Verlag.