uml模型与形式模型双向转换的研究

《uml模型与形式模型双向转换的研究》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、2011届研究生硕士学位论文学校代号：10269学号：5108150004l葶震吁筋天嗲UML模型与形式模型双向转换的研究院系：软件学院专业名称：_—■祆砰工蓰厂研究方向：——丽亿历程■一指导教师：—1f育碡r1碣羽虿硕士研究生：————颜■F一二零一一年五月一令一一，牛丑月DISSERliATIoNFORMASTERDEGREE．20llllllIIllllllllm㈣舢1111l㈣川mⅢI{Y1903714SchoolCode：10269StudentNumber：5l08l50004lEA

2、STCⅡ丑ⅡNAN⑩RMALUNⅡVERSⅡTVResearchonBi．1YansformationbetweenUMLModelsandFormalModelsDep砒ment：SoftwareEngineeringInstituteMajor：Subject：Tutor：Author：SoftwareEngineeringFormalMethodAssociateProf．DuY．ugenYanWd2011．05华东师范大学学位论文原创性声明郑重声明：本人呈交的学位论文《UML模型与形式模

3、型双向转换的研究》，是在华东师范大学攻读硬乡缝士(请勾选)学位期间，在导师的指导下进行的研究工作及取得的研究成果。除文中已经注明引用的内容外，本论文不包含其他个人已经发表或撰写过的研究成果。对本文的研究做出重要贡献的个人和集体，均已在文中作了明确说明并表示谢意。作者签名：迎日期：如“年岁月≥／日华东师范大学学位论文著作权使用声明《uML模型与形式模型双向转换的研究》系本人在华东师范大学攻读学位期间在导师指导下完成的硬≠／博士(请勾选)学位论文，本论文的研究成果归华东师范大学所有。本人同意华东师范

4、大学根据相关规定保留和使用此学位论文，并向主管部门和相关机构如国家图书馆、中信所和“知网’’送交学位论文的印刷版和电子版；允许学位论文进入华东师范大学图书馆及数据库被查阅、借阅；同意学校将学位论文加入全国博士、硕士学位论文共建单位数据库进行检索，将学位论文的标题和摘要汇编出版，采用影印、缩印或者其它方式合理复制学位论文。本学位论文属于(请勾选)()1．经华东师范大学相关部门审查核定的“内部”或“涉密”学位论文母，于年／月同解密，解密后适用上述授权。(、．．y2．不保密，适用上述授权。翩签名趣亟生

5、：b本人签名弘Ⅶi【年≮月7fR}“涉密”学位论文麻是已经华尔师范人学学位评定委员会办公室或保密委员会审定过的学位论文(需附获批的《华尔师范人学研究生申请学位论文“涉密”审批表》方为有效)，未经上述部门审定的学位论文均为公开学位论文。此卢明栏不填写的，默认为公开学位论文，均适川上述授权)。．，。颜卫硕士学位论文答辩委员会成员名单姓名职称单位备注曹奇英教授东华大学主席曾振柄教授华东师范大学刘静教授华东师范大学王长波副教授华东师范大学琚小明副教授华东师范大学毛宏燕讲师华东师范大学秘书摘要UML提供了

6、图形概念来表示面向对象软件系统的设计。在软件设计领域，它已经成为了事实上的工业标准。然而UML缺乏精确语义且是一种半形式化语言。形式化规格语言试图为软件开发提供一种精确的、完备规格说明方法。许多研究者做了许多研究工作来把UML模型转换到形式模型以分析和验证UML模型。但是由于很难证明形式描述和非形式描述之间的等价性，因此需要在两个领域之间进行不断的来回往复。凶此需要形式模型逆向转换回到UML模型。Z语言易于描述软件系统的静态结构，因此本文首先利用UMLTranZ的方法实现了uML模型到形式模型的

7、转换。UMLTranz方法能够将UML概念类图转换到Z模型。Z模型的主要架构是Schema，它能够形式的描述uML概念类图的语义。利用现存的形式模型分析工具可以对Z模型进行分析推理和证明。xMI(xMLMetamodelInterchange)是由OMG提供的模型交换数据格式。利用XMI提供的传送模型不剧部分的机制，我们提出了一种形式模型逆向转换UML模型的转换方法。这种逆向转换方法是一种间接的逆向转换方法，它能够在最大程度上减少uML模型转换到形式模型过程中所产生的弱化影响。将这种逆向转换方法

8、与现有正向的转换方法向结合就能成功的实现UML模型和形式模型之间的双向转换。我们还利用了U，rP理论形式的证明了逆向转转换方法的正确性和可行性。对应于通过UMLl’ranZ所得到的Z模型，我们基于一阶逻辑谓词和集合论定义了Z模型到UML概念类图的逆向转换具体映射规则。利用所定义的映射规则，可以间接的实现z模型到UML概念类图的逆向转换。将这种逆向转换技术和UMLTranZ结合在一起，我们就能实现UML和Z之间的双向转换。最后我们设计了一个模型双向转换工具，并利用JaVa语言开发了一个原型。关键词