毕业设计：文献参考（12）
一、基本信息
- 标题：基于UML2.0模型的测试与验证方法
- 来源：西安电子科技大学
- 作者：张琛
二、研究背景
随着信息技术的飞速发展，软件规模和复杂性不断增大，对软件开发速度和质量的要求不断提高。从而迫切需要一套简单易行的方法来指导规模庞大、结构复杂的软件开发过程。模型可以简明、准确的表示复杂、抽象的系统，并且可以帮助设计者从全局上把握系统的全貌及其相关部件之间的联系，防止设计者过早地陷入各个模块的细节之中。因此，在面向对象的软件开发中，建模就显得尤为重要，建模语言也一直是面向对象技术的研究重点。
三、具体内容
本文共有七章，具体章节如下:
第一章为绪论部分。首先，讨论了形式化方法的必要性和重要性，常用形式化验证方法的基本原理、适用范围，以及多种时序逻辑的语法和特点。然后，介绍了基于模型的测试方法，并对基于UML模型进行测试、验证的相关工作进行了分析与比较。最后，详细说明了本文的研究重点和主要工作。
第二章研究UML2.0序列图的形式化描述方法。首先，简要介绍了UML2.0序列图的新特征。然后，给出了序列图的语法、语义，以及序列图中单个对象的形式化定义。最后，定义了一种事件确定有限自动机作为序列图的形式化模型，并给出了该自动机的构造算法。
第三章研究基于UML2.0序列图的形式化验证方法。在讨论命题投影时序逻辑的语法和语义基础上，详细说明了对软件性质的描述方法以及基于事件确实有限自动机的PPTL性质模型检测算法。
第四章在对序列图形式化描述基础上，提出了基于自动机的测试用例生成方法。首先，给出了复合自动机的定义，并介绍了4种合成规则，以此为基础实现了自动机合成算法。然后，通过定义的覆盖准则、测试场景产生规则，以及测试用例生成算法产生相应的测试用例集。
第五章研究分布式软件系统交互行为的建模、验证与测试方法。首先，通过定义的系统状态机图和对象状态机图分别对分布式系统中各独立子系统的状态转换进行建模，并使用序列图建模各子系统的交互行为。然后，采用模型检测方法完成对交互行为的验证。最后，讨论了分布式软件的测试框架和基于模型的测试用例产生。
第六章详细介绍了序列图的建模工具。说明了基于Eclipse插件的序列图建模环境的设计，以及序列图向事件确实有限自动机模型进行转换的实现。
第七章是全文的总结与展望。总结了本文的工作，并对进一步的研究方向作出展望
四、参考文献
[1]张琛. 基于UML2.0模型的测试与验证方法[D].西安电子科技大学,2012.