基于多项式约束求解的程序路径测试用例生成研究

发布时间：2018-08-22 19:58

【摘要】：软件测试作为软件工程的基本过程之一,是确保软件质量的重要方法。测试用例自动生成技术作为软件测试的重要内容之一,能够增加软件测试的准确性、有效降低测试成本,具有广阔的发展前景。当前最常用的测试用例自动生成技术之一,就是符号执行。然而,基于符号执行的测试用例自动生成技术目前存在明显的不足之处:在遇到复杂的非线性浮点约束时其效果并不理想,主要体现在非线性约束的复杂性导致的求解困难和浮点计算的精度限制导致的求解不准确两个方面。目前,C语言是应用最广泛的编程语言,能够对C语言程序进行测试用例自动生成具有很高的实用价值。本文给出了一个基于多项式约束求解的测试用例生成方法,并根据这个方法开发了一款针对C语言数值程序的测试用例自动生成工具。本文的具体研究内容,包括以下三个方面:●研究符号执行技术,选择支持C语言和浮点数的符号执行工具KLEE-FP,通过符号执行技术提取程序中的路径约束。进一步,设计分析路径约束的方法,将通过KLEE-FP得到的路径约束转换为多项式约束。●对于从C语言程序中得到的每一条路径对应的多项式约束,研究如何更快、更准确地求解。一方面,研究了基于低秩矩量矩阵恢复的多项式系统求解方法,对于含有等式和不等式的复杂多项式系统,该方法求解速度更快、更适合大规模问题的求解;另一方面,研究了基于区间分析的验证算法,通过计算出包含准确实解的区间并基于该区间给出测试用例,来有效地避免浮点计算导致的不准确和异常。●实现了一款测试用例自动生成工具ATCase(Automatically generate Test Case),能够分析C语言数值程序中的路径并自动生成满足该路径约束的测试用例。总的来说,对于给定的C语言数值程序,首先通过符号执行技术提取程序路径约束并转换为多项式约束,然后通过多项式约束求解的可验证算法得到满足路径约束的测试用例。本文根据这个过程开发了一款软件ATCase,并通过实验验证了 ATCase的高效性和强健壮性。
[Abstract]:As one of the basic processes of software engineering, software testing is an important method to ensure software quality. As one of the important contents of software testing, automatic test case generation technology can increase the accuracy of software testing and reduce the test cost effectively. It has a broad development prospect. One of the most commonly used test case generation techniques is symbolic execution. However, the automatic test case generation technique based on symbolic execution has some obvious shortcomings: the effect is not satisfactory when complex nonlinear floating point constraints are encountered. It is mainly reflected in two aspects: the difficulty of solving due to the complexity of nonlinear constraints and the inaccuracy caused by the precision limitation of floating-point calculation. At present, C language is the most widely used programming language. It has high practical value to automatically generate test cases for C language programs. In this paper, a test case generation method based on polynomial constraint solution is presented. Based on this method, a test case generation tool for C language numerical programs is developed. The specific research contents of this paper include the following three aspects: research on symbolic execution technology, select symbol execution tool KLEE-FPwhich supports C language and floating-point number, extract path constraints in program by symbolic execution technology. Furthermore, the method of analyzing path constraints is designed to convert the path constraints obtained by KLEE-FP into polynomial constraints. For the polynomial constraints corresponding to each path obtained from C language programs, how to solve them faster and more accurately is studied. On the one hand, the method of solving polynomial systems based on the restoration of low rank moment matrix is studied. For complex polynomial systems with equality and inequality, the method is faster and more suitable for solving large-scale problems. The verification algorithm based on interval analysis is studied. By calculating the interval containing quasi-exact solution, the test cases are given based on the interval. An automatic test case generation tool, ATCase (Automatically generate Test Case), is implemented to analyze the paths in C language numerical programs and automatically generate test cases that meet the path constraints. In general, for a given C language numerical program, the program path constraints are firstly extracted by symbolic execution technique and converted into polynomial constraints, and then the test cases satisfying the path constraints are obtained by a verifiable algorithm for solving polynomial constraints. According to this process, a software ATCase is developed in this paper, and the high efficiency and strong robustness of ATCase are verified by experiments.
【学位授予单位】：华东师范大学
【学位级别】：硕士
【学位授予年份】：2017
【分类号】：TP311.53

【参考文献】