基于模型检测的UML一致性检验与测试用例生成

摘要

随着计算机软件应用的深入，人们对软件的质量和可靠性提出了更高的要求，通常采用系统建模和软件测试来保障。模型检测作为一种形式化的验证技术，有着自动化和提供反例等诸多优点。因此，本文的主要研究工作是利用模型检测技术来实现统一建模语言UML一致性检验和测试用例自动生成，从而来保证软件的高可靠性。
　　UML是一种描述能力强大且涵义直观的可视化建模语言，然而由UML得到的表示系统多个方面的模型之间存在着一定的信息冗余和相互交织，从而可能会产生不一致性问题。本文提出了一套UML2.0中顺序图和状态图到SMV语言的转换准则，解决了顺序图中的组合片段和异步消息等特性。把状态图和顺序图分别表示为SMV语言模型和CTL时序逻辑，使用模型检测工具NuSMV进行一致性检验。最后，基于以上研究工作，设计并开发了UML检验工具。
　　软件测试是保障软件质量的关键步骤，其核心问题是测试用例的自动生成。本文在研究了基于模型检测的测试用例自动生成方法的基础上，提出了一个基于二叉树快速生成算法来构造时序逻辑；结合基于需求、运用模型检测技术的测试用例自动生成流程，得到满足MC/DC覆盖准则的测试用例集。最后，设计并实现了一个基于模型检测的测试用例自动生成工具，结合航空电子系统，利用现有工具TestBed进行测试用例的正确性和覆盖率的验证。

目录

封面

声明

中文摘要

英文摘要

目录

图表清单

缩略词

第一章 绪论

1.1 研究背景及意义

1.2 国内外研究现状

1.3 论文研究内容

1.4 论文组织结构

第二章 理论背景

2.1 模型检测理论

2.2 时序逻辑

2.3 模型检测工具NuSMV

2.4 UML概述

2.5 软件测试

2.6 本章小结

第三章 UML顺序图与状态图一致性检验

3.1 UML与模型检测技术相结合的建模过程

3.2 UML状态图

3.3 UML顺序图

3.4 顺序图与状态图的一致性检验

3.5 模型检验工具的实现

3.6 实例应用

3.7 本章小结

第四章 满足MC/DC准则的测试用例生成

4.1 运用模型检测生成测试用例的方法

4.2 基于MC/DC准则的时序逻辑构造方法

4.3 运用模型检测生成测试用例的流程

4.4 测试用例自动生成工具的实现与验证

4.5 本章小结

第五章 总结与展望

5.1 全文总结

5.2 未来展望

参考文献

致谢

在学期间的研究成果及发表的学术论文