{log} as a Test Case Generator for the Test Template Framework

{log} (pronounced ‘setlog’) is a Constraint Logic Programming (CLP) 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 Zermelo-Fraenkel set theory 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 the Zermelo-Fraenkel 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} performs better than ProB for this application.