基于SPIN的UML模型一致性验证的研究及应用

摘要

随着计算机技术的高速发展，软件系统的复杂性和规模也越来越高，为了解决大型软件系统的设计和开发问题，UML提供了多种面向对象分析和设计的建模视图，支持对各种复杂系统进行可视化分析、设计和软件部署。然而，由于UML缺乏精确的形式化描述和语义定义，使得各种视图之间很难保证模型的一致性和正确性。近年来，模型的一致性和正确性检测成为一个非常突出和重要的研究课题，但目前的大多数研究方法是通过人工审查或形式化推理等半自动的方式进行检测，不适合工业化应用。模型检测技术是一种快速、全自动的形式化验证方法，本文针对UML模型之间存在语义重叠和信息冗余等问题，结合SPIN检测工具对UML模型进行正确性和一致性验证，本文所做的工作如下：
　　首先，综合分析了UML类图、活动图和时序图的元素，采用严格的形式化对其语法和语义进行描述；由于对UML模型执行一致性检测须保证模型本身的正确性，同时对带有嵌套结构的多层次活动图难以解析其模型元素和不易实现自动化验证，因此提出以树形结构对多层次活动图进行分解，并对分解完成的简单子图进行标准化和完整性检测；继而提出 UML活动图到Promela模型的转换规则和Promela模型的重组算法，从而实现了多层次活动图活性及可靠性的验证。
　　接着，针对类图、时序图与活动图之间的一致性问题，定义了时序图消息的顺序关系以及UML模型之间的一致性语义，基于消息的顺序关系对时序图消息进行约简，从而实现了时序图对象的交互行为到活动图控制轨迹的转换；继而通过详细分析 SPIN的验证机制，提出基于同步的一致性映射规则和检测算法，并结合检测工具SPIN实现了UML模型的类型一致性和行为一致性的自动化验证。
　　最后，根据活动图的正确性验证算法和UML模型之间的一致性检测算法，以Eclipse Plug-in为开发框架，开发了UML模型一致性验证工具；继而将该验证工具应用于“攻防对抗系统”实例中，经实验表明，验证工具能准确识别和解析 UML模型，并且成功检测出模型存在的一致性问题。

目录

封面

声明

中文摘要

英文摘要

目录

缩略词

第一章 绪论

1.1引言

1.2研究现状

1.3课题的研究内容

1.4论文的组织结构

第二章 UML模型与模型检测

2.1 UML语言的体系结构

2.2一致性分类和检测方法

2.3 SPIN模型检测技术

第三章 UML活动图的正确性验证

3.1 UML模型形式化定义

3.2多层次活动图的分解与标准化

3.3针对活动图的正确性验证

3.4本章小结

第四章 基于进程同步的模型转换及验证方法

4.1一致性定义

4.2时序图到活动图的转换算法

4.3基于进程同步的模型验证算法

4.4一致性验证方法及实验分析

4.5本章小节

第五章 基于一致性验证的系统建模工具的实现与应用

5.1基于一致性验证的系统建模工具的实现

5.2系统建模工具在攻防对抗系统中的应用

5.3本章小结

第六章 总结和展望

6.1论文的工作总结

6.2后续工作展望

参考文献

致谢

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