Abstract
Recent advances in propositional satisfiability (SAT) and Satisfiability Modulo Theories (SMT) solvers are increasingly rendering SAT and SMT-based automatic test generation an attractive alternative to traditional algorithmic test generation methods. The use of SAT/SMT solvers is particularly appealing when testing Boolean expressions. The main advantages are the capability to deal with constraints over the models, the generation of compact test suites, and the support for fault detecting test generation methods. However, these solvers require normally more time and greater amount of memory than classical test generation algorithms, making their applicability not always feasible in practice. In this paper we propose several ways to optimize the process of test generation and we compare several SAT/SMT solvers and propositional transformation rules. These optimizations promise to make SAT/SMT-based techniques as efficient as standard methods for testing purposes, especially when dealing with Boolean expressions, as proved by our experiments.
Recent advances in propositional satisfiability (SAT) and Satisfiability Modulo Theories (SMT) solvers are increasingly rendering SAT and SMT-based automatic test generation an attractive alternative to traditional algorithmic test generation methods. The use of SAT/SMT solvers is particularly appealing when testing Boolean expressions. The main advantages are the capability to deal with constraints over the models, the generation of compact test suites, and the support for fault detecting test generation methods. However, these solvers require normally more time and greater amount of memory than classical test generation algorithms, making their applicability not always feasible in practice. In this paper we propose several ways to optimize the process of test generation and we compare several SAT/SMT solvers and propositional transformation rules. These optimizations promise to make SAT/SMT-based techniques as efficient as standard methods for testing purposes, especially when dealing with Boolean expressions, as proved by our experiments.
Papers
Angelo Gargantini, Gordon Fraser
Generating minimal fault detecting test suites for general Boolean specifications
Information and Software Technology, Volume 53, Issue 11, pp. 1263-1273
Paolo Arcaini, Angelo Gargantini, Elvinia Riccobene
Optimizing the automatic test generation by SAT and SMT solving for Boolean expressions
Automated Software Engineering conference ASE 2011: 388-391
Paolo Arcaini, Angelo Gargantini, Elvinia Riccobene
How to Optimize the Use of SAT and SMT Solvers for Test Generation of Boolean Expressions
The Computer Journal, 58 (11) (2015) 2900-2920
Angelo Gargantini, Gordon Fraser
Generating minimal fault detecting test suites for general Boolean specifications
Information and Software Technology, Volume 53, Issue 11, pp. 1263-1273
Paolo Arcaini, Angelo Gargantini, Elvinia Riccobene
Optimizing the automatic test generation by SAT and SMT solving for Boolean expressions
Automated Software Engineering conference ASE 2011: 388-391
Paolo Arcaini, Angelo Gargantini, Elvinia Riccobene
How to Optimize the Use of SAT and SMT Solvers for Test Generation of Boolean Expressions
The Computer Journal, 58 (11) (2015) 2900-2920
Tool
Download tg_boolean.jar
usage:
java -jar tg_boolean.jar [options] "expression"
options:
-collect : use collect
-fault [ASF | ENF | MVF | ORF | SA1 | SA0 | VNF | CCF | CDF | VRF] : list of fault classes (repeat switch), empty for all
-noreduce : do not reduce after generation
-noskipcovered : do not skip tps already covered
-solver [SAT4J | YICES] : solver (default SAT4j)
-time : show time information
-verbose : be verbose
example:
java -jar tg_boolean.jar -fault ASF -fault ENF "a or b"
notes:
the Yices version will be completed soon - for now use SAT4j
Download tg_boolean.jar
usage:
java -jar tg_boolean.jar [options] "expression"
options:
-collect : use collect
-fault [ASF | ENF | MVF | ORF | SA1 | SA0 | VNF | CCF | CDF | VRF] : list of fault classes (repeat switch), empty for all
-noreduce : do not reduce after generation
-noskipcovered : do not skip tps already covered
-solver [SAT4J | YICES] : solver (default SAT4j)
-time : show time information
-verbose : be verbose
example:
java -jar tg_boolean.jar -fault ASF -fault ENF "a or b"
notes:
the Yices version will be completed soon - for now use SAT4j
Benchmarks
- TACAS specifications
- Random specifications - 160k specifications randomly generated, with a different number of variables (#ids) and height of the expression syntectic tree (#depth). For each combination of #ids and #depth (with 1 <= #ids <= 20 and 1 <= #depth <= 80) there are 100 specifications. Each specification has an unique identifier of the form random_#ids_#depth_#count, where #count is a counter over the specifications with given #ids and #depth.
- Toughest random specifications - 34 random specifications that were the toughest to solve in our experiments.
- Specifications derived from Java code, ISCAS models and NuSMV models - Each specification is composed by a Boolean expression and a constraint. For each specification the number of occurrences in the original models is reported (since several of the retrieved specification are equal up to isomorphism).
- Most frequent specifications - Specifications representing the 99% of the specifications retrieved from Java code, ISCAS models and NuSMV models.