Towards Efficient Data-flow Test Data Generation

Overview

Data-flow testing (DFT) checks the correctness of variable definitions by observing their corresponding uses. It has been empirically proved to be more effective than control-flow testing in fault detection, however, its complexities still overwhelm the testers in practice. To tackle this problem, we introduce a hybrid testing framework: (1) The core of our framework is symbolic execution, enhanced by a novel guided path search to improve testing performance; and (2) we systematically cast DFT as reachability checking in software model checking to complement SE, yielding practical DFT that combines the two techniques’ strengths. We implemented our framework on the state-of-the-art symbolic execution tool KLEE and model checking tools BLAST, CPAchecker and CBMC, and extensively evaluate it on 30 real-world subjects with collectively 22,793 def-use pairs. The enhanced SE approach not only covers more pairs, but also reduces testing time by 10∼43%. The model checking approach can effectively weed out infeasible pairs that KLEE cannot infer by 70.1∼95.8%. Finally, for all subjects, our hybrid approach can improve data-flow coverage by 28.7∼46.3%, and reduce testing time by up to 64.6% than the symbolic execution approach alone. This hybrid approach also enables the cross-checking of each component for reliable and robust testing results.

Approach Workflow

Tools (Download)

Our approach was built on four different tools, which are summarized as follows.

Our version of KLEE can be downloaded, which is adapted for data-flow testing.

Name Approach Technique Version
KLEE Symbolic Execution SE v1.1.0
BLAST Model Checking CEGAR v2.7.3
CPAchecker Model Checking CEGAR v1.6.1
CBMC Model Checking BMC v5.6

Benchmark (Download)

We carefully constructed a repository of benchmark subjects for evaluating data-flow testing techniques. It includes subjects from three sources:

CBMC uses --unwind and --depth, respectively, to limit the number of times loops to be unwound and the number of program steps to be processed. The parameters used in our evaluation are listed below.

Name CBMC's --unwind CBMC's --depth
factorization 4 90
power 2 40
find 4 90
triangle 2 40
strmat 3 60
strmat2 3 70
textfmt 25 700
tcas 2 200
replace 6 350
totinfo 15 250
printtokens 30 300
printtokens2 12 450
schedule 5 350
schedule2 5 250
kbfiltr 2 250
kbfiltr2 2 300
diskperf 2 650
floppy 2 500
floppy2 2 500
cdaudio 2 500
s3_clnt 13 500
s3_clnt_termination 13 400
s3_srvr_1a 10 200
s3_srvr_1b 4 100
s3_srvr_2 15 1450
s3_srvr_7 15 1450
s3_srvr_8 15 1450
s3_srvr_10 15 600
s3_srvr_12 15 1500
s3_srvr_13 15 1500

Summary of Results

For more information, please feel free to contact us: Ting Su, Chengyu Zhang, Yichen Yan.

Reference

Last modified: 2018.3