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

发布时间：2018-01-19 18:51

本文关键词： 测试用例自动生成符号执行多项式系统实根求解低秩矩量矩阵恢复　出处：《系统科学与数学》2017年07期 　论文类型：期刊论文

【摘要】：现有的基于符号执行的测试用例自动生成技术存在不足之处:由于精度限制和非线性约束求解的复杂性,符号执行在遇到复杂的非线性浮点约束时效果并不理想.针对这一现状,给出了一个基于多项式约束求解和区间验证的测试用例生成算法.对于复杂非线性约束难以求解的问题,采用基于低秩矩量矩阵恢复的多项式系统求解方法,该方法对于含有等式和不等式的多项式系统,相较于其他方法求解速度更快,更适合大规模问题的求解;对于浮点约束求解不准确的问题,采用基于区间分析的验证算法来计算包含精确实解的区间,基于该区间给出测试用例,可以避免浮点计算的不准确和异常.结合该算法和符号执行工具KLEE-FP实现了一个测试用例自动生成工具ATCase(automatically generate test case),它能够分析数值程序中的路径并自动生成满足路径约束的测试用例.在两个开源软件库中的2两个复杂的真实程序上运行的实验结果表明ATCase相比KLEE-FP所使用的STP求解器,能快速生成具有更高覆盖率的测试用例,特别是在处理相对复杂的非线性约束时,优势更加明显.
[Abstract]:The existing automatic test case generation techniques based on symbolic execution have some shortcomings: because of the precision limitation and the complexity of solving nonlinear constraints. Symbolic execution does not work well when complex nonlinear floating point constraints are encountered. A test case generation algorithm based on polynomial constraint solution and interval verification is presented. For the problem with complex nonlinear constraints, a polynomial system solution method based on the restoration of low rank moment matrix is adopted. This method is more suitable for solving large-scale problems than other methods for polynomial systems with equality and inequality. For the inexact solution of floating point constraints, a verification algorithm based on interval analysis is used to calculate the interval containing the exact solution, and the test cases are given based on the interval. This algorithm is combined with the symbol execution tool KLEE-FP to implement an automatic test case generation tool ATCase (. Automatically generate test case. It can analyze paths in numerical programs and automatically generate test cases satisfying path constraints. The experimental results on two complex real programs in two open source software libraries show that ATCase is better than KL. The STP solver used by EE-FP. It can quickly generate test cases with higher coverage, especially when dealing with relatively complex nonlinear constraints.
【作者单位】：华东师范大学上海市高可信计算重点实验室;温州大学数学与信息科学学院;中国科学院数学与系统科学研究院数学机械化重点实验室;南京大学计算机软件新技术国家重点实验室;
【基金】：国家重点研发计划项目(2016YFB1000802) 国家自然科学基金项目(61632015,61561146394,61602348) 上海市自然科学基金项目(17ZR1408300)资助课题
【分类号】：TP311.53
【正文快照】： i引言软件测试是软件工程的基本过程,是确保软件质量和可靠性的重要方法,它相当于观察软件系统的执行是否和预期的相同,以此来确定潜在的故障w.在软件开发过程中,以往的人工测试的成本占了50%-80%,而且容易出错、不能面面俱到然而,随着软件的复杂性、广泛性和关键性不断增加,

【相似文献】