Applying SMT Solvers to the Test Template Framework

Details Applying SMT Solvers to the Test Template Framework Applying SMT Solvers to the Test Template Framework

2012-02-28

arxiv.org/abs/1202.6120v1

EPTCS 80, 2012, pp. 28-42

Computer Science

Software Engineering

In Proceedings MBT 2012, arXiv:1202.5826

Scientific paper

10.4204/EPTCS.80.3

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.

Affiliated with

Also associated with

No associations

Rating

Applying SMT Solvers to the Test Template Framework does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Applying SMT Solvers to the Test Template Framework, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Applying SMT Solvers to the Test Template Framework will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-605549