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

论文摘要

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

论文目录

• 摘要
• ABSTRACT
• 第一章 绪论
• 1.1 研究背景及意义
• 1.2 国内外研究现状
• 1.3 论文研究内容
• 1.4 论文组织结构
• 第二章 理论背景
• 2.1 模型检测理论
• 2.1.1 模型检测原理
• 2.1.2 模型检测过程
• 2.1.3 Kripke 结构
• 2.2 时序逻辑
• 2.2.1 计算树时序逻辑 CTL*
• 2.2.2 线性时序逻辑 LTL
• 2.2.3 分支时序逻辑 CTL
• 2.3 模型检测工具 NuSMV
• 2.3.1 NuSMV 的基本结构
• 2.3.2 NuSMV 输入语言 SMV
• 2.4 UML 概述
• 2.4.1 UML 简介
• 2.4.2 UML 语言体系结构
• 2.4.3 UML 模型的一致性
• 2.5 软件测试
• 2.5.1 软件测试的方法
• 2.5.2 测试用例自动生成方法
• 2.6 本章小结
• 第三章 UML 顺序图与状态图一致性检验
• 3.1 UML 与模型检测技术相结合的建模过程
• 3.2 UML 状态图
• 3.2.1 状态图介绍
• 3.2.2 状态图语法
• 3.2.3 状态图转换
• 3.3 UML 顺序图
• 3.3.1 顺序图介绍
• 3.3.2 顺序图语法
• 3.3.3 顺序图转换
• 3.4 顺序图与状态图的一致性检验
• 3.5 模型检验工具的实现
• 3.5.1 检验工具的设计
• 3.5.2 检验工具的实现
• 3.6 实例应用
• 3.7 本章小结
• 第四章 满足 MC/DC 准则的测试用例生成
• 4.1 运用模型检测生成测试用例的方法
• 4.1.1 运用模型检测生成测试用例的原理
• 4.1.2 主要技术途径
• 4.2 基于 MC/DC 准则的时序逻辑构造方法
• 4.2.1 MC/DC 准则
• 4.2.2 MC/DC 准则的形式化定义
• 4.2.3 MC/DC 准则的算法设计
• 4.2.4 算法分析与验证
• 4.3 运用模型检测生成测试用例的流程
• 4.3.1 根据需求规格形式化建模
• 4.3.2 根据 MC/DC 准则构造时序逻辑
• 4.3.3 运用模型检测工具进行验证
• 4.3.4 从反例中提取测试用例
• 4.4 测试用例自动生成工具的实现与验证
• 4.4.1 航空电子系统测试过程
• 4.4.2 测试用例生成工具的设计
• 4.4.3 测试用例生成工具的实现与验证
• 4.4.4 在 TestBed 中执行测试用例
• 4.5 本章小结
• 第五章 总结与展望
• 5.1 全文总结
• 5.2 未来展望
• 参考文献
• 致谢
• 在学期间的研究成果及发表的学术论文