UML顺序图和状态图的形式化方法研究

论文摘要

统一建模语言(Unified Modeling Language,UML)是一种描述能力强大且含义直观的可视化建模语言,它提供多种视图从不同角度和应用层次刻画系统特性以及复杂的运行环境。UML语法结构虽然采用了形式化的规约,但其语义部分则是用自然语言来描述。容易产生模糊或歧义。因此,对UML进行形式化语义研究,可以增进该语言的准确性、一致性和可扩展性。UML2.0版本的顺序图经常用于描述并发系统的设计需求,反映对象之间的动态交互关系,着重体现对象之间消息传递的时间顺序,因此,用一个恰当的时序逻辑描述语言来给出它的语义是可行的。XYZ/E是一种可执行的线性时序逻辑语言,既可描述系统的动态行为又可表示程序性质,对顺序图进行形式化规约后,可在统一的时序逻辑框架下分析顺序图的性质。论文给出了一个改进的顺序图语法定义,同时对现有的基于XYZ/E时序逻辑语言的UML顺序图语义进行了深入研究,针对存在的问题,根据给出的语法定义,提出了新的解决方案,更加精确地描述了顺序图的语义。UML支持用户从不同的角度对系统建模,不同视图间存在着信息的冗余,如顺序图和状态图在描述动态行为上存在着重叠,因此可能导致视图间不一致的产生。首先,论文介绍了形式化模型检验方法的原理和特点,阐述了模型检验工具SPIN的原理和语法。其次,针对顺序图逻辑语义多样性的特点,提出了一种分析方法,同时给出了新的语义定义。再次,提出一个更全面的状态图语法定义,并针对状态图的复杂层次结构特性,引入有限状态自动机,提出自动机分解算法FSADA,经分解后得到自动机树。最后,提出新的顺序图和状态图的一致性检验准则、Promela代码结构,以及将状态图转换成Promela代码的ATTP算法,并用模型检验工具SPIN实现了两者之间的一致性检验。

论文目录

• 摘要
• ABSTRACT
• 第一章 绪论
• 1.1 引言
• 1.2 研究现状
• 1.3 本文主要工作及组织结构
• 第二章 UML形式化研究
• 2.1 UML语言体系结构
• 2.1.1 UML四层元模型体系结构
• 2.1.2 存在的问题
• 2.2 UML形式语义的研究
• 2.3 UML模型的一致性
• 2.3.1 UML模型一致性问题产生的原因
• 2.3.2 UML模型一致性分类方案
• 2.3.3 UML模型一致性检测方法
• 2.4 本章小结
• 第三章 UML2.0顺序图的XYZ/E时序逻辑语义研究
• 3.1 UML顺序图
• 3.1.1 UML2.0顺序图新特征概述
• 3.1.2 UML顺序图形式化语义的研究现状
• 3.2 时序逻辑语言XYZ/E
• 3.2.1 XYZ/E连接词
• 3.2.2 XYZ/E时序算子
• 3.2.3 XYZ/E基本命令格式
• 3.3 UML顺序图的语法
• 3.4 UML顺序图的语义
• 3.4.1 顺序图语义的二义性
• 3.4.2 基于XYZ/E的顺序图语义
• 3.5 实验
• 3.5.1 实例描述
• 3.5.2 实例分析
• 3.6 本章小结
• 第四章 UML2.0顺序图与状态图的一致性研究
• 4.1 顺序图与状态图的一致性问题
• 4.1.1 相关研究
• 4.1.2 验证UML模型语义一致性的一般方法
• 4.2 状态图
• 4.2.1 状态图的概述
• 4.2.2 UML状态图的语法
• 4.2.3 有限状态自动机
• 4.2.4 分解有限状态自动机
• 4.3 UML顺序图的语义分析
• 4.4 模型检验
• 4.4.1 模型检验过程
• 4.4.2 时态逻辑
• 4.4.3 模型检验工具SPIN
• 4.5 顺序图与状态图的一致性检验
• 4.5.1 一致性检验准则
• 4.5.2 顺序图转换成Promela
• 4.5.3 有限状态自动机转换成Promela
• 4.5.4 实验
• 4.6 本章小结
• 第五章 结束语
• 参考文献
• 致谢
• 附录