Greedy Combinatorial Test Case Generation using Unsatisfiable Cores
Akihisa Yamada, Armin Biere, Cyrille Artho, Takashi Kitamura, and Eun-Hye ChoiProceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering (ASE 2016), pp. 614 – 624, 2016.
Abstract
Combinatorial testing aims at covering the interactions of parameters in a
system under test, while some combinations may be forbidden by given
constraints (forbidden tuples).
In this paper, we illustrate that such forbidden tuples correspond to
unsatisfiable cores, a widely understood notion in the SAT solving community.
Based on this observation, we propose a technique to detect forbidden tuples
lazily during a greedy test case generation, which significantly reduces the
number of required SAT solving calls. We further reduce the amount of time
spent in SAT solving by essentially ignoring constraints while constructing
each test case, but then ``amending’‘ it to obtain a test case that satisfies
the constraints, again using unsatisfiable cores. Finally, to complement a
disturbance due to ignoring constraints, we implement an efficient
approximative SAT checking function in the SAT solver Lingeling.
Through experiments we verify that our approach significantly improves
the efficiency of constraint handling in our greedy combinatorial testing
algorithm.
BibTeX
@inproceedings{AY-ASE2016, author = "Akihisa Yamada and Armin Biere and Cyrille Artho and Takashi Kitamura and Eun-Hye Choi", title = "Greedy Combinatorial Test Case Generation using Unsatisfiable Cores", booktitle = "Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering (ASE 2016)", pages = "614--624", publisher = "ACM", year = 2016 }