• 论文 • 上一篇    下一篇

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

王砺磊 1,曾霞1 ,林望2,3 ,陈鑫4 , 杨争峰1   

  1. 1. 华东师范大学上海市高可信计算重点实验室, 上海 200062; 2. 温州大学数学与信息科学学院, 温州 325035;3. 中国科学院数学与系统科学研究院数学机械化重点实验室,北京100190; 4. 南京大学计算机软件新技术国家重点实验室, 南京 210023
  • 出版日期:2017-07-25 发布日期:2017-09-30

王砺磊,曾霞,林望,陈鑫,杨争峰. 一个基于多项式约束求解的数值程序测试用例自动生成工具[J]. 系统科学与数学, 2017, 37(7): 1704-1721.

An Automatic Generation Tool of Test Case for Numerical Program Based on Polynomial Constraint Solving

WANG Lilei 1, ZENG Xia 1 ,LIN Wang 2,3 ,CHEN Xin4 ,YANG Zhengfeng1   

  1. 1. Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai 200062; 2. College of Mathematics and Information Science, Wenzhou University, Wenzhou 325035; 3. Key Laboratory of Mathematics Mechanization, Chinese Academy of Sciences, Beijing 100190;4. State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing 210023
  • Online:2017-07-25 Published:2017-09-30

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

The existing symbolic execution approach of automatic test case generation is defective because of the precision restrict and complexity for solving non-linear constrains, which make the result not satisfactory. For this deficiency, a test case generation algorithm based on polynomial system solving technique and interval verification is provided. Concretely, for the difficulty of solving non-linear constrains aspect, low-rank moment matrix recover based method to solve polynomial system is utilized, which is more efficient and suitable for big scale problems. For the inaccuracy results from computation, we make good use of interval arithmetic at the computation procedure to provide an interval containing the real root of the system and then choose the test case from it as the result, which is more accurate avoiding false test cases from the computational error. In this paper, an automatic generation tool of test case for numerical program named ATCase is proposed. The theoretical bases of ATCase are the algorithm of computing real solutions of polynomial constraints, the interval analysis and the symbolic execution tool KLEE-FP. Experiments on 22 complicated real programs in open source projects show that the proposed tool is more effective and efficient than the STP solver of KLEE-FP, especially in case of complex non-linear constraints.

()
No related articles found!
阅读次数
全文


摘要