Multi-thread Combinatorial Test Generation with SMT solvers
Open Access
- 27 March 2023
- conference paper
- Published by Association for Computing Machinery (ACM)
- p. 1698-1705
Abstract
Combinatorial interaction testing (CIT) is a testing technique that has proven to be effective in finding faults due to the interaction among inputs and in reducing the number of test cases, without losing effectiveness. Several tools have been proposed in the literature; however, generating tests remains a challenging task. In this paper, we present a technique for generating combinatorial test suites that uses a multi-thread architecture and exploits Satisfiability Modulo Theory (SMT) solvers to represent model parameters, constraints, and tuples, and it builds from SMT solver contexts the desired test suite. This technique is implemented by the tool KALI. The main advantage of using SMT solvers is that combinatorial models can contain all kinds of parameters and constraints. To evaluate our approach, we tested the impact of several optimizations and compared the performance of KALI with those of some existing tools for test generation. Our experiments confirm that the use of multi-threading is a promising technique but still requires some optimization for being more effective than the already available ones.Keywords
This publication has 13 references indexed in Scilit:
- CHiP: A Configurable Hybrid Parallel Covering Array ConstructorIEEE Transactions on Software Engineering, 2018
- Yices 2.22014
- The MathSAT5 SMT Solver2013
- Experimentation in Software Engineering2012
- SMTInterpol: An Interpolating SMT Solver2012
- MC-MIPOG: A Parallel t-Way Test Generation Strategy for Multicore SystemsETRI Journal, 2010
- Interaction Coverage Meets Path Coverage by SMT Constraint SolvingLecture Notes in Computer Science, 2009
- A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic2008
- Z3: An Efficient SMT Solver2008
- Online testing with model programsACM SIGSOFT Software Engineering Notes, 2005