Applying SMT Solvers to the Test Template Framework

TL;DR

This paper explores the use of SMT solvers Yices and CVC3 to generate test cases from Z notation specifications within the Test Template Framework, demonstrating initial feasibility and embedding techniques.

Contribution

It introduces the first application of SMT solvers to TTF for Z notation, including shallow embeddings of Z into SMT solver input languages.

Findings

SMT solvers successfully generate test cases from Z specifications

Shallow embeddings enable compatibility with SMT solvers

Initial results show promise for automated test case generation

Abstract

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 with equality and Zermelo-Fraenkel set theory. In this way, a test case is a witness satisfying a formula in that theory. Satisfiability Modulo Theory (SMT) solvers are software tools that decide the satisfiability of arbitrary formulas in a large number of built-in logical theories and their combination. In this paper, we present the first results of applying two SMT solvers, Yices and CVC3, as the engines to find test cases from TTF's test specifications. In doing so, shallow embeddings of a significant portion of the Z notation into the input languages of Yices and CVC3 are provided, given that they do not directly support Zermelo-Fraenkel set theory as defined in Z. Finally, the results of applying these embeddings to a number of test specifications of eight cases studies are analysed.