Bidirectional Symbolic Analysis for Effective Branch Testing

Structural coverage metrics, and in particular branch coverage, are popular approaches to measure the thoroughness of test suites. Unfortunately, the presence of elements that are not executable in the program under test and the difficulty of generating test cases for rare conditions impact on the effectiveness of the coverage obtained with current approaches. In this paper, we propose a new approach that combines symbolic execution and symbolic reachability analysis to improve the effectiveness of branch testing. Our approach embraces the ideal definition of branch coverage as the percentage of executable branches traversed with the test suite, and proposes a new bidirectional symbolic analysis for both testing rare execution conditions and eliminating infeasible branches from the set of test objectives. The approach is centered on a model of the analyzed execution space. The model identifies the frontier between symbolic execution and symbolic reachability analysis, to guide the alternation and the progress of bidirectional analysis towards the coverage targets. The experimental results presented in the paper indicate that the proposed approach can both find test inputs that exercise rare execution conditions that are not identified with state-of-the-art approaches and eliminate many infeasible branches from the coverage measurement. It can thus produce a modified branch coverage metric that indicates the amount of feasible branches covered during testing, and helps team leaders and developers in estimating the amount of not-yet-covered feasible branches. The approach proposed in this paper suffers less than the other approaches from particular cases that may trap the analysis in unbounded loops.