一句话:将最优 concolic 测试策略归约为带代价马尔可夫决策过程,并提出贪心近似算法。
concolic 测试结合具体执行与符号执行生成测试用例,但其策略(何时随机测试、何时符号执行及选择哪条路径)多依赖启发式,最优策略仍是开放问题。本文首先证明最优策略可由程序路径概率与约束求解代价定义,并将寻找最优策略归约为带代价的马尔可夫决策过程(MDP with Costs)的模型检测问题。由于精确求解该问题复杂,作者进一步设计贪心算法以近似最优策略。评估包含随机生成模型和一组 C 程序两组实验,结果表明现有启发式仍有较大改进空间,且所提贪心算法通常优于现有启发式。
Concolic testing integrates concrete execution (e.g., random testing) and symbolic execution for test case generation. It is shown to be more cost-effective than random testing or symbolic execution sometimes. A concolic testing strategy is a function which decides when to apply random testing or symbolic execution, and if it is the latter case, which program path to symbolically execute. Many heuristics-based strategies have been proposed. It is still an open problem what is the optimal concolic testing strategy. In this work, we make two contributions towards solving this problem. First, we show the optimal strategy can be defined based on the probability of program paths and the cost of constraint solving. The problem of identifying the optimal strategy is then reduced to a model checking problem of Markov Decision Processes with Costs. Secondly, in view of the complexity in identifying the optimal strategy, we design a greedy algorithm for approximating the optimal strategy. We conduct two sets of experiments. One is based on randomly generated models and the other is based on a set of C programs. The results show that existing heuristics have much room to improve and our greedy algorithm often outperforms existing heuristics.