● 摘要
软件测试是软件质量保证的重要手段，测试用例的设计是软件测试中的基本问题。人工测试用例设计依赖于测试人员的经验，耗时耗力，并且不能保证测试覆盖率。测试用例的自动生成可以极大地节省人力，提高软件质量的可信度。本文围绕“基于符号演算的单元测试用例自动生成的研究”这一课题，研究了如何将符号演算和模型检验这两种方法相结合，实现基于修订的条件/判定覆盖的单元测试用例的自动生成。 本文先对国内外相关领域的研究状况进行调研，并介绍了目前比较常用的自动用例生成法——随机法和启发式搜索算法。但是，由于测试用例输入空间的无界性和程序逻辑的复杂性，基于结构覆盖的测试用例自动生成问题一直没有很好的解决。然后，本文借助形式化验证技术，以修订的条件/判定覆盖为目标，提出一种单元测试用例自动生成方法，它将模型检验和符号演算相结合，将程序中的变量符号化，探测程序可能的执行路径，并收集每条路径执行必须满足的条件，再通过求解路径条件集从而得出每条路径的测试用例。本文详细阐述了基于模型检验器Java PathFinder的符号演算扩展。在数据类型方面，引入了符号类型数据的定义，并描述这些符号数据在代码执行过程中的存储与传递方式，其中重点阐述数组类型的符号数据在符号执行时的处理方法，即对数组的组成元素单独演算，此外还对数组混淆问题提出了解决策略；在控制结构方面，采用决策技术遍历程序中的每个分支的条件，并使用循环控制迭代算法确定循环的迭代次数，以覆盖特定条件。本文接着详细介绍了用例生成工具原型的设计和实现。最后对方法的有效性进行实例验证。