Suitability analysis of CSP- and SMT-solvers for test case generation
Hermann Felbinger, Christian Schwarzl · 2014
Model-based testing allows automatic test case generation from models like Symbolic Input Output Transition Systems (SIOTS) describing the behavior of the System under Test (SUT). In order to create feasible test inputs a Constraint Satisfaction Problem (CSP)-solver or a Satisfiability Modulo Theory (SMT)-solver can be used. The test input creation complexity depends amongst others on the variable domains, the variable number and the test length. Since the capabilities of a test generation from a given SIOTS strongly depends on the used CSP- or SMT-solver, the most suitable one has to be selected. In this paper we benchmarked commonly used CSP- and SMT-solvers like Minion, Choco, Z3 or CVC4, regarding their time needed to solve constraints typical in model-based testing. The experimental results show that the compared solvers can differ vastly regarding the number of correctly solved and the time needed for a set of constraints. Since the solver performance depends on the characteristics of the constraint to be solved, no winner can be named. However, the provided results allow the selection of the most suitable solver for dedicated problem sets.