UML顺序图与状态图一致性检验

摘要

近年来，软件规模的不断扩大，复杂度不断增加，如何提高软件开发效率，保证软件的质量成为软件工业界的关键性问题。统一面向对象建模技术为提高大规模软件开发的效率与质量带来了希望，为软件开发自动化奠定了基础。统一面向对象软件建模语言UML以其图形化的表达及对软件设计提供各种各样的支持而迅速成为软件业界的标准。开发人员可以使用多种角度对系统进行建模，但是不同视图模型可能存在信息冗余，可能导致视图不一致性等问题。因此，对UML进行形式化描述与研究，给出UML准确的形式化定义，可以提高该语言的准确性、扩展性和一致性。 UML顺序图常用于描述并发系统的设计需求，着重体现对象之间消息传递的时间顺序，因此，用一个适当的时序逻辑描述语言来给出它的语义是可行的。XYZ/E是一种可执行的线性时序逻辑语言，既可描述系统的动态行为又可表示程序性质，对顺序图进行形式化规约后，可在统一的时序逻辑框架下分析顺序图的性质。论文给出了一个改进的顺序图语法定义，同时对基于XYZ/E时序逻辑语言的UML顺序图语义进行了深入研究，针对存在的问题，根据给出的语法定义，提出了新的解决方案，更加精确地描述了顺序图的语义。 本文主要是对具有多种逻辑语义的顺序图提出语义分析方法，为复杂层次结构的状态图引入自动机，应用自动机算法得到自动机树，同时制定了新的顺序图与状态图的一致性检测准则，用模型检验工具SPIN对顺序图与其相关的状态图进行一致性检测。

目录

文摘

英文文摘

声明

第一章绪论

1.1背景介绍

1.2研究现状

1.3论文的研究方法

1.4论文的组织结构

第二章 UML2.0顺序图时序逻辑语言XYZ／E的研究

2.1形式化方法与规范语言

2.2时序逻辑语言XYZ／E的简介

2.3 XYZ／E连接词及时序算子

2.4 XYZ／E基本命令格式

2.5 UML顺序图的基本语法与语义

2.6实验

2.7本章小结

第三章UML形式化研究

3.1UML语言体系结构

3.2 UML形式化语义的研究

3.3 UML模型的一致性

3.4本章小结

第四章 UML2.0顺序图与状态图的一致性研究

4.1顺序图与状态图一致性问题

4.2状态图

4.3 UML顺序图的语义分析

4.4模型检验

4.5顺序图与状态图的一致性检验

4.6本章小结

第五章 结束语

参考文献

致谢