Combining Symbolic Execution and Model Checking for Data Flow Testing
Ting Su, Zhoulai Fu, Geguang Pu, Jifeng He, Zhendong Su · 2015
Abstract—Data flow testing (DFT) focuses on the flow of data through a program. Despite its higher fault-detection ability over other structural testing techniques, practical DFT remains a significant challenge. This paper tackles this challenge by intro-ducing a hybrid DFT framework: (1) The core of our framework is based on dynamic symbolic execution (DSE), enhanced with a novel guided path search to improve testing performance; and (2) we systematically cast the DFT problem as reachability checking in software model checking to complement our DSE-based approach, yielding a practical hybrid DFT technique that combines the two approaches ’ respective strengths. Evaluated on both open source and industrial programs, our DSE-based approach improves DFT performance by 60∼80 % in terms of testing time compared with state-of-the-art search strategies, while our combined technique further reduces 40 % testing time and improves data-flow coverage by 20 % by eliminating infeasible test objectives. This combined approach also enables the cross-checking of each component for reliable and robust testing results. I.