论文部分内容阅读
高可信软件技术是软件理论研究和工程实践领域关注的焦点之一。近年来，越来越多的形式化方法被应用于提高软件质量的研究上。软件测试是保证软件产品可靠性和正确性的有效手段之一，而模型检测是一种确保设计规范正确性的形式化自动验证技术。研究发现，模型检测中生成的反例可有效应用于测试用例的生成，显著减少测试代价，提高软件质量。本文主要研究基于模型检测的类测试自动生成技术。本文分别采用数据流测试和变异测试的方法，并结合模型检测器Java PathFinder(JPF)，将测试生成问题简化成模型检测中寻找反例的问题，提出了两种面向对象软件测试用例自动生成的方法。首先采用数据流测试的方法，通过设置陷阱性质，用时序逻辑公式表示数据流测试的覆盖准则，提出一种自动生成测试用例的方法，并在JPF上实现。该方法满足数据流覆盖准则，适用于Java类内方法间调用序列的测试。算法分析与实验结果表明，通过设置适当的搜索深度，本文提出的算法使得类数据流测试的覆盖率提高了8％，并能发现隐藏在程序当中的错误；通过本文提出的方法调用选择原则，可显著减少生成调用序列的长度；与JPF的DFS算法相比，本文提出的算法减少了搜索过程中产生的冗余状态，并及时进行了回退，在内存消耗基本相同的情况下本文算法生成的新状态数减少了65％，回退次数减少了90％，处理的状态数减少了88％，算法的执行时间也减少了28％，有效减少了测试生成的代价。此外，基于变异测试的思想，采用类复制的方法，应用JPF来保证软件执行过程中产生的错误在输出结果中可见，自动生成满足变异覆盖准则的测试用例，适用于类之间方法调用的测试，从而实现了Java类之间的测试用例自动生成。算法分析与实验结果表明，针对TreeMap类的测试用例生成实验，本文提出的方法覆盖了其中主要的面向对象特性，且生成的变异数多达211个，而反例数仅26个就覆盖了100％的有效变异，显著减少了测试生成的代价；与Visser提出的模型检测器JPF上的符号执行方法相比，在对TreeMap类中的deleteEntry、fixAfterDeletion和fixAfterInsertion三个方法进行测试用例生成的实验中，本文提出的方法有效覆盖率达到了100％，覆盖率提高了约15％，且本文提出的方法不依赖于程序结构的设计，并能保证程序执行过程中出现的错误在输出结果中表现出来，以发现隐藏的错误。