UML活动图模型检测方法的研究

摘要

随着人们对软件正确性和安全性的要求越来越高，高可信软件工程技术得到了研究人员的广泛关注。在高可信软件工程中，模型检测以其简洁明了和自动化程度高而倍受瞩目。模型检测是一种重要的形式化自动验证技术，其中SPIN是一种著名的分析验证系统逻辑一致性的模型检测工具，输入语言是PROMELA语言。
　　统一建模语言UML是一种半形式化建模语言，缺乏精确的语义描述。本文研究了UML活动图与模型检测两者之间的结合，主要研究内容包括以下几点：
　　1、在UML的各种图形中，活动图易于理解，用于对系统的动态行为建模。本文研究了活动图中的节点及语义，活动图由事件流将整个活动过程串联在一起的，消息的发送和接受是随着事件流进行的。
　　2、实现了UML活动图到PROMELA语言的转换。首先将UML活动图转换成XML语言，然后再将XML语言转换成PROMELA语言，经历了这样两次转换，其中第一次转换：将UML语言转换成XML使用建模工具StarUML来实现的，本文中用MFC实现了将活动图的XML语言转换成PROMELA语言的过程。
　　3、总结了PROMELA语言建模的一般规律，并在活动图模型检测过程中实践了这一规律。通过分析UML活动图的XML文件内部表示形式，将活动图定义为一个五元组，A=，其中P:状态的有限集合；M:事件流的有限集合；T:事件流的分类，提出了将事件流分为common和special两种形式，其中common指的是令牌为空的情况，special指的是令牌不为空的情况；O:事件流的下一个对象；I:事件流的来源。
　　本文设计并实现了UML活动图的转换工具，最后以图书馆借书活动图为例，用SPIN工具验证了该活动图。

目录

封面

声明

中文摘要

英文摘要

目录

第一章 绪论

§1-1研究背景和意义

§1-2相关研究基础和现状

§1-3 论文的主要工作

§1-4 本文的组织结构

第二章 模型检测及相关技术

§2-1 模型检测简介

§2-2模型检测优化技术

§2-3时态逻辑

第三章 用PROMELA对系统建模

§3-1 系统建模工作流程

§3-2 模型检测工具SPIN及PROMELA语言

§3-3 用PROMELA对系统建模

第四章 UML活动图到PROMELA语言的转换

§4-1 UML活动图

§4-2 活动图模型转换过程

§4-3 活动图转换实例

第五章 活动图模型转换工具的设计与实现

§5-1活动图模型检测过程

§5-2转换工具的设计与实现

第六章 结论

§6-1 结论

§6-2展望

参考文献

致谢

附录A