基于模型检测的类测试自动生成技术研究

摘要

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

目录

文摘

英文文摘

第一章引言

1.1软件测试与模型检测

1.2论文的主要工作

1.3论文的组织

第二章模型检测理论基础

2.1基本概念

2.2模型检测工具

2.3模型检测研究进展

2.4程序模型检测器JAVA PATHFINDER

2.4.1 JPF的发展

2.4.2在应用程序中使用Verify

2.4.3 JPF中解决状态爆炸问题的机制

2.5本章小结

第三章软件测试用例自动生成方法

3.1软件测试的发展

3.2软件测试技术

3.3测试用例自动生成方法研究进展

3.2.1随机测试数据生成方法

3.2.2符号执行测试技术

3.2.3遗传算法、模拟退火算法和禁忌搜索算法

3.2.4数据流方法

3.2.5变异测试方法

3.4软件测试中的模型检测方法应用研究

3.5本章小结

第四章基于JPF的类数据流测试生成方法

4.1类数据流测试方法研究进展

4.2类数据流分析和测试

4.3基于JPF的类数据流测试方法

4.3.1测试方法框架

4.3.2测试生成算法描述

4.4实例分析

4.4.1对CoinBox类的测试生成方法分析

4.4.2实验结果

4.5本章小结

第五章基于类复制变异的类间测试用例自动生成方法

5.1类变异测试研究进展

5.2变异分析和测试

5.2.1变异测试的状态机描述

5.2.2变异算子的选择

5.2.3变异错误的输出可视化

5.3基于JPF和类间变异的测试用例生成方法

5.3.1测试实例：红黑树

5.3.2基于类复制的测试用例生成方法

5.4实验结果

5.5本章小结

第六章总结与展望

6.1本文的主要工作与贡献

6.2进一步的研究工作

参考文献

致谢

攻读硕士学位期间参加的科研项目

攻读硕士学位期间录用发表的学术论文