ATCase:一个基于多项式约束求解的数值程序测试用例自动生成工具

作     者：王砺磊 曾霞 林望 陈鑫 杨争峰 WANG Lilei ZENG Xia LIN Wang CHEN Xin YANG Zhengfeng

作者机构：华东师范大学上海市高可信计算重点实验室上海200062 温州大学数学与信息科学学院温州325035 中国科学院数学与系统科学研究院数学机械化重点实验室北京100190 南京大学计算机软件新技术国家重点实验室南京210023 

出 版 物：《系统科学与数学》 (Journal of Systems Science and Mathematical Sciences)

年 卷 期：2017年第37卷第7期

页      面：1704-1721页

核心收录：

学科分类：08[工学] 0835[工学-软件工程] 081202[工学-计算机软件与理论] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：国家重点研发计划项目(2016YFB1000802) 国家自然科学基金项目(61632015,61561146394,61602348) 上海市自然科学基金项目(17ZR1408300)资助课题 

主　　题：测试用例自动生成 符号执行 多项式系统实根求解 低秩矩量矩阵恢复. 

摘      要：现有的基于符号执行的测试用例自动生成技术存在不足之处:由于精度限制和非线性约束求解的复杂性,符号执行在遇到复杂的非线性浮点约束时效果并不理想.针对这一现状,给出了一个基于多项式约束求解和区间验证的测试用例生成算法.对于复杂非线性约束难以求解的问题,采用基于低秩矩量矩阵恢复的多项式系统求解方法,该方法对于含有等式和不等式的多项式系统,相较于其他方法求解速度更快,更适合大规模问题的求解;对于浮点约束求解不准确的问题,采用基于区间分析的验证算法来计算包含精确实解的区间,基于该区间给出测试用例,可以避免浮点计算的不准确和异常.结合该算法和符号执行工具KLEE-FP实现了一个测试用例自动生成工具ATCase(automatically generate test case),它能够分析数值程序中的路径并自动生成满足路径约束的测试用例.在两个开源软件库中的2两个复杂的真实程序上运行的实验结果表明ATCase相比KLEE-FP所使用的STP求解器,能快速生成具有更高覆盖率的测试用例,特别是在处理相对复杂的非线性约束时,优势更加明显.