软件测试作为软件工程的基本过程之一,是确保软件质量的重要方法。测试用例自动生成技术作为软件测试的重要内容之一,能够增加软件测试的准确性、有效降低测试成本,具有广阔的发展前景。当前最常用的测试用例自动生成技术之一,就是符号执行。然而,基于符号执行的测试用例自动生成技术目前存在明显的不足之处:在遇到复杂的非线性浮点约束时其效果并不理想,主要体现在非线性约束的复杂性导致的求解困难和浮点计算的精度限制导致的求解不准确两个方面。目前,C语言是应用最广泛的编程语言,能够对C语言程序进行测试用例自动生成具有很高的实用价值。本文给出了一个基于多项式约束求解的测试用例生成方法,并根据这个方法开发了一款针对C语言数值程序的测试用例自动生成工具。本文的具体研究内容,包括以下三个方面:●研究符号执行技术,选择支持C语言和浮点数的符号执行工具KLEE-FP,通过符号执行技术提取程序中的路径约束。进一步,设计分析路径约束的方法,将通过KLEE-FP得到的路径约束转换为多项式约束。●对于从C语言程序中得到的每一条路径对应的多项式约束,研究如何更快、更准确地求解。一方面,研究了基于低秩矩量矩阵恢复的多项式系统求解方法,对于含有等式和不等式的复杂多项式系统,该方法求解速度更快、更适合大规模问题的求解;另一方面,研究了基于区间分析的验证算法,通过计算出包含准确实解的区间并基于该区间给出测试用例,来有效地避免浮点计算导致的不准确和异常。●实现了一款测试用例自动生成工具ATCase(Automatically generate Test Case),能够分析C语言数值程序中的路径并自动生成满足该路径约束的测试用例。总的来说,对于给定的C语言数值程序,首先通过符号执行技术提取程序路径约束并转换为多项式约束,然后通过多项式约束求解的可验证算法得到满足路径约束的测试用例。本文根据这个过程开发了一款软件ATCase,并通过实验验证了 ATCase的高效性和强健壮性。