集成图形化规格说明和形式方法的研究

摘要

在软件开发过程中,多数用户需求的规格说明采用非形式的自然语言或半形式的图表结构进行描述,由于非形式方法的模糊性和歧义性,产生的规格说明往往不够精确和完整,规格说明的不同使用者对于同一规格说明会有不同的理解,从而造成系统的不完善.形式方法基于严格的数学逻辑,以形式推理和定理证明为工具推导程序,能提供精确的规格说明.形式方法虽然具有精确、无二义性的特点,但由于它需要设计者有较好的数学基础,因此不容易为人们所接受.图形化规格说明和形式方法都可以用于软件开发的需求分析和设计阶段,有很大的互补性.本文就是以UML和Object-Z为例,研究如何在软件需求分析阶段集成图形化规格说明和形式方法,以获得精确的软件需求规格说明.本文从整个系统的角度分析了如何实现从用户需求到图形化规格说明描述,再到形式规格说明:首先结合一个例子,介绍了如何使用UML来描述系统的Use Case视图、Logical视图、Component视图和Deployment视图.接着从这个实例出发,对该模型的Use Case视图和Logical视图进行形式化,系统地研究了UML类图、用例图、顺序图、状态图到Object-Z的转换,在总结前人的基础上,通过形式化各种UML模型中的元模型,提出了自己关于UML到Object-Z的一个比较系统的转换规则.根据本文提出的规则,可以实现一个简单系统的UML规格说明到形式规格说明的转换.为了支持本文提出的理论方法,开发了基于XMI(XML Metadata Interchange)的工具UMLFormalizer,实现了UML模型到Object-Z的自动转换.

目录

文摘

英文文摘

原创性声明及本论文使用授权说明

致谢

第一章引言

1.1软件需求简介

1.2主要工作

1.3相关工作

第二章图形规格说明与形式方法

2.1图形规格说明简介

2.1.1 Booch方法

2.1.2 Coad/Yourdon方法

2.1.3OMT

2.1.4 Jacobson方法

2.1.4 UML[2][14]

2.2形式方法简介

2.2.1形式方法的主要优点

2.2.2Z

2.2.3 Object-Z

2.3图形规格说明与形式方法的集成

2.3.1集成图形规格说明与形式方法的意义

2.3.2集成图形规格说明与形式方法的可行性

第三章使用UML描述系统

3.1引例

3.2 RationalRose简介

3.3描述系统的Use case视图

3.3.1捕获角色

3.3.2捕获用例

3.4描述系统的Logical视图

3.4.1使用顺序图实现用例

3.4.2设计类图

3.4.3设计类的状态图

3.5描述系统的Component视图

3.6描述系统的Deployment视图

第四章使用Object-Z形式化UML模型

4.1形式化UML的方法简介

4.1.1 UML的架构

4.1.2 UML的元模型

4.1.3使用形式语言Object-Z形式化UML的元模型

4.2类图的形式化

4.2.1类的形式化

4.2.2关系的形式化

4.2.3关联类的形式化

4.2.4系统类的形式化

4.3顺序图的形式化

4.3.1消息的形式化

4.3.2顺序图的形式化

4.4用例图的形式化

4.5状态图的形式化

4.5.1状态

4.5.2迁移

4.5.3形式化整个状态图

第五章形式化工具UMlFormalizer的设计和实现

5.1 XMI简介

5.2解析XMI

5.2.1 XMI文档的结构

5.2.2 DOM简介

5.2.3解析过程

5.3 Obiect-Z的输出

5.3.1 Object-Z的显示

5.3.2特殊字符的处理

5.3.3 Obiect-Z的保存

5.4 UMLFormalizer功能简介

结束语

参考文献

论文说明