使用uml和event-b构建基于云平台的应用软件模型

《使用uml和event-b构建基于云平台的应用软件模型》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、江苏科技大学硕士学位论文使用UML和Event-B构建基于云平台的应用软件模型专业名称：软件工程作者姓名：夏志龙指导教师：高尚江苏科技大学学位论文原创性声明本人郑重声明：所呈交的学位论文，是本人在导师的指导下，独立进行研究工作所取得的成果。除文中已经注明引用的内容外，本论文不包含任何其他个人或集体已经发表或撰写过的作品成果。对本文的研究做出重要贡献的个人和集体，均已在文中以明确方式标明。本人完全意识到本声明的法律结果由本人承担。学位论文作者签名：夏志龙2016年04月05日摘要软件工程实践中广泛采用UML（UnifiedM

2、odelingLanguage）作为建模语言，UML是一种语言，也可以称其为一种技术。UML具有半形式化的特点，它的形式化部分使其具有严密和精确的特点，它的非形式化部分使其易于接受和推广。UML模型构件的结构采用形式化描述，而相应的语义采用自然语言描述，这是将UML称为半形式化技术的原因之一。另外，UML技术可以对模型进行形式化的描述，但是UML技术本身没有指出如何对模型进行形式化验证，这是将UML称为半形式化技术的原因之二。事实上，UML的半形式化特点固然使其易于使用、易于推广，但是不能支持一些软件工程的应用场景。如果需要分析

3、软件模型演进的一致性，这是单独使用UML技术不能做到的。UML模型在软件工程的不同阶段会持续演进，演进过程中会引入UML模型一致性问题。使用UML不能分析此问题，这是因为UML技术本身无法进行模型验证。可以采用其他形式化分析技术协助分析UML模型的一致性。Event-B就是这样一种形式化技术，它可以形式化的描述模型，也可以对模型进行形式化验证。如何将UML技术和Event-B技术结合是本文的重点。要实现两种技术的结合，需要开发基于Event-B技术分析UML模型一致性的一整套方法。本文提出了UML模型向Event-B模型转换的规

4、则和算法设计方法；设计了具体的转换算法，并证明了这些算法的规范性；并且证明了采用这些算法转换得到的Event-B模型和原UML模型的语义一致性，进而证明了它们的等价性；在上述基础上，本文提出了基于Event-B形式化分析UML模型一致性的方法，并将此方法应用于改进一个基于云平台的应用软件模型。本文的主要内容包括如下几个方面：首先分析了UML技术半形式化特点带来的好处与问题，介绍了克服这些问题的研究进展，并提出了可以将Event-B和UML结合的方法和思路。其次介绍了UML技术，包括UML的元-元模型和元模型以及UML建模的一般过

5、程。还介绍了Event-B技术，包括Event-B模型的元-元模型和元模型以及Event-B技术的Rodin平台。接着研究了UML模型向Event-B模型转换的方法，包括转换规则和实现算法，并且证明了算法的规范性以及模型转换的等价性。并且在前述提出的模型转换规则和算法的基础上，提出了基于Event-B形式化分-I-析UML模型演进一致性的方法，并且通过案例演示了该方法的一般使用过程。最后构建了一个基于云平台的应用软件UML模型，并且将前述提出的基于Event-B形式化分析UML模型演进一致性的方法应用于此UML模型的建模过程，呈

6、现了该方法对UML模型的改进。从应用结果看，本文提出的基于Event-B形式化分析UML模型一致性的方法是有效的，可以支持分析、设计人员的工作，可以在软件工程的分析和设计阶段作为支撑UML模型质量改进的有效方法。关键词：UML；Event-B；类图；状态图；形式化分析-II-AbstractUnifiedmodelinglanguage(UML)pervadesthepracticesofsoftwareengineering.UMLisasetoftechniquesaswellasasortofmodelinglanguag

7、e.UMLisso-calledasemi-formallanguage.Ononehand,theabstractsyntaxesofUMLconstructsaredescribedbyformallanguage,butthesemanticsofUMLconstructsareportrayedbynaturelanguage.Thisisonereasontoclassifyitasasemi-formallanguage.Andontheotherhand,UMLtechniquedoesn’tspecifyhowt

8、oformallyverifyamodelbyitselfthoughitcandepictthemodelformally.ThisisanotherreasontosayUMLisasemi-formallanguage.Inpractice,theform