基于SPIN/Promela的UML模型验证工具设计与实现

论文摘要

UML是一个通用的可视化的对象建模语言,经过了近十多年的发展和完善,在软件工业中已成为占支配地位的建模语言。UML在对系统进行建模时,由于其缺少分析系统结构的准确语义,且UML内部的多视角视图之间也存在不一致性的情况。因此,对UML模型的正确性难于保证,进而也限制了UML模型的有效性。形式化方法是软件开发过程中用于分析、设计及实现系统的软件工程方法,是软件规格和验证的方法。形式化方法具有清晰、精确、抽象、简明、规范地验证软件系统及其性质的能力,能帮助发现其它方法不容易发现的系统描述的不一致等问题,有助于增加开发人员对系统的理解,能够极大地提高软件的安全性和可靠性。针对形式化方法与可视化方法的优缺点,本文基于形式化方法与可视化UML相结合的建模思想,设计了一套从UML模型到Promela模型的转换规则,用时态逻辑LTL刻画系统模型性质,开发了由UML模型自动生成Promela代码的转换工具。在转换工具中通过调用SPIN自动验证Promela代码,来验证UML模型的正确性,若UML模型与刻画的性质不一致,SPIN将给出违反系统性质的反例。通过转换工具对实例进行验证,实验结果表明此工具的有效性。

论文目录

• 摘要
• ABSTRACT
• 第1章 绪论
• 1.1 研究背景
• 1.2 研究的主要工作
• 1.2.1 研究目标
• 1.2.2 研究内容
• 1.3 论文的创新点
• 1.4 论文的结构
• 第2章 模型检测
• 2.1 模型检测概述
• 2.1.1 模型检测的基本概念
• 2.1.2 模型检测的基本原理
• 2.2 模型检测技术
• 2.2.1 模型检测主要支撑工具
• 2.2.2 SPIN的选型依据
• 2.3 模型检测工具SPIN
• 2.3.1 SPIN的工作原理
• 2.3.2 SPIN的图形界面工具XSPIN
• 2.4 PROMELA
• 2.4.1 数据类型
• 2.4.2 进程说明
• 2.4.3 信息传递
• 2.4.4 流向控制
• 2.5 线性时态逻辑 LTL
• 第3章 UML建模
• 3.1 UML概述
• 3.1.1 UML的建模元素
• 3.1.2 UML的主要特点
• 3.2 UML组成结构
• 3.2.1 UML语义
• 3.2.2 UML语法
• 3.3 UML建模机制
• 3.3.1 静态建模机制
• 3.3.2 动态建模机制
• 3.4 UML建模流程
• 3.5 小结
• 第4章 UML模型到PROMELA模型的转换
• 4.1 UML模型验证
• 4.2 UML与模型检测方法相结合的建模过程
• 4.3 UML模型到Promela模型的转换机制
• 4.4 UML模型到Promela模型的转换
• 4.4.1 UML类图（Class Diagram）的Promela转换
• 4.4.2 UML Statechart Diagram的Promela转换
• 4.4.3 UML活动图的Promela转换
• 4.4.4 UML协作图与时序图的Promela转换
• 4.5 小结
• 第5章 模型验证工具的实现
• 5.1 转换工具的设计
• 5.2 转换工具的实现
• 5.2.1 转换工具实现过程中的基本数据结构
• 5.2.2 模型验证工具的转换实现
• 5.3 模型验证工具的操作界面
• 5.4 小结
• 第6章 UML模型验证的实例分析
• 6.1 经典案例分析
• 6.2 项目案例分析
• 6.2.1 系统需求
• 6.2.2 项目的 UML用例图和类图
• 6.3 小结
• 第7章 结论和展望
• 7.1 总结
• 7.2 进一步研究工作
• 致谢
• 参考文献
• 攻读学位期间的研究成果