一种基于符号执行的测试用例生成方法

A Test Case Generation Method Based on Symbolic Execution

针对符号执行中存在的路径爆炸问题,提出一种冗余路径删除方法,该方法利用Hoare逻辑中的后置条件引导符号执行以生成有效的测试用例。首先利用最弱前置条件来计算已探索的路径,然后通过后置条件引导符号执行以识别程序中多个共享的路径后缀,并在测试用例生成时进行消除。最后通过对多个基准程序进行实验,结果表明论文方法在一定程度上能够减少程序的路径探索数目和执行时间,削弱了符号执行中的路径爆炸问题。

Aiming at the problem of path explosion existing in the execution of symbols,a redundant path deletion method is proposed,which uses the postconditions in the Hoare logic to guide symbol execution to generate effective test cases. The weakened preconditions are first used to calculate the explored paths and then the postconditions are used to guide the execution of the symbols to identify multiple shared path suffixes in the program and eliminate them as test cases are generated. Finally,by testing a number of benchmark programs,the results show that this method can reduce the number of program exploration and execution time to a cer. tain extent,and weaken the path explosion in symbol execution.