Refining CEGAR-Based Test-Case Generation with Feasibility Annotations
摘要
Often, testing is part of software quality assurance, in which testers may use automatic tools to generate test cases. To avoid redundant work, the tools may consider collateral coverage, i.e., use that a test case generated for a particular test goal, e.g., a branch, may cover further goals. We present a novel approach to use collateral coverage during test-case generation with software model checkers that apply counterexample-guided abstraction refinement. For every test goal, those model checkers perform a reachability analysis, which we plan to support with previous test inputs. More concretely, we use a feasibility annotation to map already covered goals to their test inputs. Whenever the reachability analysis detects a syntactical path to an uncovered test goal, we select a test input from the feasibility annotation that is likely a (partial) input for the path and use this input as a potential guide to check whether the path is semantically feasible. So far, we have integrated our approach into and evaluated it on the Test-Comp tasks. Compared to the original approach, our approach performs similar or better. In total, we increase the achieved branch coverage by 2%, but may achieve a significantly larger increase for some tasks.