使用UML和Event-B构建基于云平台的应用软件模型

发布时间：2017-04-04 21:03

  本文关键词：使用UML和Event-B构建基于云平台的应用软件模型，由笔耕文化传播整理发布。

【摘要】：软件工程实践中广泛采用UML(Unified Modeling Language)作为建模语言,UML是一种语言,也可以称其为一种技术。UML具有半形式化的特点,它的形式化部分使其具有严密和精确的特点,它的非形式化部分使其易于接受和推广。UML模型构件的结构采用形式化描述,而相应的语义采用自然语言描述,这是将UML称为半形式化技术的原因之一。另外,UML技术可以对模型进行形式化的描述,但是UML技术本身没有指出如何对模型进行形式化验证,这是将UML称为半形式化技术的原因之二。事实上,UML的半形式化特点固然使其易于使用、易于推广,但是不能支持一些软件工程的应用场景。如果需要分析软件模型演进的一致性,这是单独使用UML技术不能做到的。UML模型在软件工程的不同阶段会持续演进,演进过程中会引入UML模型一致性问题。使用UML不能分析此问题,这是因为UML技术本身无法进行模型验证。可以采用其他形式化分析技术协助分析UML模型的一致性。Event-B就是这样一种形式化技术,它可以形式化的描述模型,也可以对模型进行形式化验证。如何将UML技术和Event-B技术结合是本文的重点。要实现两种技术的结合,需要开发基于Event-B技术分析UML模型一致性的一整套方法。本文提出了UML模型向Event-B模型转换的规则和算法设计方法;设计了具体的转换算法,并证明了这些算法的规范性;并且证明了采用这些算法转换得到的Event-B模型和原UML模型的语义一致性,进而证明了它们的等价性;在上述基础上,本文提出了基于Event-B形式化分析UML模型一致性的方法,并将此方法应用于改进一个基于云平台的应用软件模型。本文的主要内容包括如下几个方面:首先分析了UML技术半形式化特点带来的好处与问题,介绍了克服这些问题的研究进展,并提出了可以将Event-B和UML结合的方法和思路。其次介绍了UML技术,包括UML的元-元模型和元模型以及UML建模的一般过程。还介绍了Event-B技术,包括Event-B模型的元-元模型和元模型以及Event-B技术的Rodin平台。接着研究了UML模型向Event-B模型转换的方法,包括转换规则和实现算法,并且证明了算法的规范性以及模型转换的等价性。并且在前述提出的模型转换规则和算法的基础上,提出了基于Event-B形式化分析UML模型演进一致性的方法,并且通过案例演示了该方法的一般使用过程。最后构建了一个基于云平台的应用软件UML模型,并且将前述提出的基于Event-B形式化分析UML模型演进一致性的方法应用于此UML模型的建模过程,呈现了该方法对UML模型的改进。从应用结果看,本文提出的基于Event-B形式化分析UML模型一致性的方法是有效的,可以支持分析、设计人员的工作,可以在软件工程的分析和设计阶段作为支撑UML模型质量改进的有效方法。
【关键词】：UML Event-B 类图 状态图 形式化分析
【学位授予单位】：江苏科技大学
【学位级别】：硕士
【学位授予年份】：2016
【分类号】：TP311.5;TP393.09
【目录】：

• 摘要3-5
• Abstract5-13
• 第一章 绪论13-21
• 1.1 选题背景13-15
• 1.2 研究现状和相关工作15-18
• 1.2.1 形式化方法和技术15-16
• 1.2.2 UML与其它形式化技术的结合16-18
• 1.3 本文主要工作18-19
• 1.4 本文组织结构19-21
• 第二章 UML和Event-B技术21-35
• 2.1 统一建模语言UML21-24
• 2.1.1 UML元-元模型和元模型21-22
• 2.1.2 UML模型的图22-23
• 2.1.3 UML建模的一般过程23-24
• 2.2 形式化技术Event-B24-31
• 2.2.1 Event-B元-元模型和元模型25
• 2.2.2 Event-B模型的构件25-28
• 2.2.3 Event-B模型的证明义务28-30
• 2.2.4 Event-B技术的Rodin平台30-31
• 2.3 基于云平台的软件模型31-32
• 2.3.1 云平台对模型的约束31-32
• 2.3.2 模型在云平台上部署32
• 2.4 本章小结32-35
• 第三章 UML模型向Event-B模型的转换方法35-51
• 3.1 模型转换过程和形式化35-38
• 3.1.1 模型转换过程的形式化35-36
• 3.1.2 Event-B模型的形式化重定义36-37
• 3.1.3 UML模型的形式化重定义37-38
• 3.2 模型转换的规则和算法38-46
• 3.2.1 模型转换规则和算法的设计过程38
• 3.2.2 模型转换算法实现和规范性证明38-46
• 3.3 模型转换的等价性46-49
• 3.3.1 模型等价性的假设46-48
• 3.3.2 模型等价性的证明48-49
• 3.4 本章小结49-51
• 第四章 基于Event-B的模型演进一致性分析方法51-65
• 4.1 模型演进的一致性51-54
• 4.1.1 Event-B模型的证明义务之证明51-52
• 4.1.2 Event-B模型演进相关证明义务52-54
• 4.2 模型演进一致性分析54-63
• 4.2.1 模型演进一致性分析的过程54
• 4.2.2 模型演进一致性分析的案例54-57
• 4.2.3 案例输出结果的分析57-59
• 4.2.4 案例中模型的转换细节59-62
• 4.2.5 案例中证明的推导方法62-63
• 4.3 本章小结63-65
• 第五章 应用一致性分析方法改进基于云平台的应用软件模型65-91
• 5.1 建立基于云平台的应用软件UML模型65-81
• 5.1.1 UML需求模型65-70
• 5.1.2 UML分析模型70-74
• 5.1.3 UML设计模型74-80
• 5.1.4 UML部署模型80-81
• 5.2 验证UML模型的一致性81-87
• 5.2.1 演进前UML模型转换81-83
• 5.2.2 演进后UML模型转换83-86
• 5.2.3 Rodin平台运行结果86-87
• 5.3 UML模型的改进87-89
• 5.3.1 Event-B模型的改进87-88
• 5.3.2 原UML模型的改进88-89
• 5.4 本章小结89-91
• 第六章 结束语91-93
• 6.1 本文总结91-92
• 6.2 未来工作92-93
• 参考文献93-97
• 攻读学位期间发表的论文97-99
• 致谢99

  本文关键词：使用UML和Event-B构建基于云平台的应用软件模型，由笔耕文化传播整理发布。

，

本文编号：285888