浅议基于动态逻辑的uml模型一致性检验

《浅议基于动态逻辑的uml模型一致性检验》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、中山大学硕士学位论文基于动态逻辑的UML模型一致性检验姓名：郑炳喜申请学位级别：硕士专业：计算机软件与理论指导教师：周晓聪20080508中山大学硕士学位论文基于动态逻辑的UML模型一致性检验专业：计算机软件与理论硕士生：郑炳喜导师：周晓聪副教授摘要在基于UML的软件开发过程中，各种UML图形从不同侧面描绘着所开发的软件系统，这些图形之间存在着信息的重叠，从而导致uML模型的一致性问题。UML模型的一致性问题也是建模过程中一个重要并且需要解决的问题。KeYTool是一个支持形式化规范和代码验证的工具，该工具基于动态逻辑对程序和形式化规范进行分析和验证，然而该工具并不支持在设计阶

2、段对UML模型进行一致性检验。作为KeYTool的基础，动态逻辑不仅具备描述程序设计语言的能力，而且能够描述UML／OCL中的动态概念。因此，研究利用动态逻辑来解决UML模型的一致性问题具有理论意义和应用价值。本论文首先对UML模型存在的一致性问题进行综述，在此基础上深入分析已有的方法，即骶g提出的利用动态逻辑来检验UML模型一致性的方法中存在的问题。Greg的方法只针对某一特定简单的UML模型进行设计，而本论文从一般UML模型的基本要素出发来分析模型转换的方法，解决了原有方法中存在的一些问题。并且，原有方法只支持类图、顺序图和状态图的检验，本论文对该方法进行扩充，增加了OCL

3、规范与其他UML图形之间的一致性检验。通过案例分析表明，改进和扩充后的方法不但能检验出更多UML图形之间的一致性问题，而且能检验出0CL约束与其他UML图形之间的一致性问题。关键词：UML，动态逻辑，一致性m中山大学硕士学位论文基于动态逻辑的眦模型一致性检验UMLModelsConsistencyCheckngBasedonDynamicLogicMajor：ComputerSo胁areandT11eo巧N锄e：BingXiZhengSupenrisor：AssociateProfessorXiaochongZhouAbstractIntlleprocessoftheUML-b

4、aSedsoR、)~raredeVeloping，aIrtifi虬tsrepresentingdi艉remaspectsofmesystemareproduced．TheoVerlappingiⅢ’o姗ation锄ongthese狐if．actsmayresultinconsiStencyproblemsoftheUMLmodels．KeYT．oolproVidesf．acilitiesforfornlalspecif；icationandVerificationofsourcecode，butitdoesnotsupportconsistencychecl(ingfordyn

5、甜11icUMLdiagrams．As也ebaseoftheKeYTbol，dynanliclogichaStheabilitytocope丽tllbothreal、阳rldprogramminglallguagesaIlddyn锄icconceptsofUML／OCL．Therefore，itisfeaSibleaJldval眦出letodeal、忻ththeconsistencyproblemwithdynaIlliclogic．111ismesisgivesaIloVenriewoft11econsistencyproblemsofUMLmodelsfirSt，andth

6、enexploresGreg’smethod，w11ichuSesdyn锄iclogicforUMLmodelconsistency．Greg’smethodomyconsidersapanicularsimpleUMLmodelauldhaSmanyotherdrawbacks．Di肫rsfromGreg’s印proach，thisthesispayspecialattentiontot11eessentialfeaturesofUMLdia铲锄sWhentmslatingUMLdia舒锄s，aIldsuppoIrtscheck洫gconsistencybet、VeenOCL

7、specificationandUMLdiagrimls．TheconsistencycheckingprocessisillustratedbyacaSestudy，w11ichalsoshowst11attlleimproVedme吐lodcaIldetectmorehndsofconsistencyproblemsofUML／OCLmodels．Keywords：UML，Dynamiclogic，ConsistencyⅣ中山大学硕士学位论文基于动态逻辑的u近模型二致罹橙验原创性声明本人