基于spin的uml活动图验证

《基于spin的uml活动图验证》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、华东师范大学硕士学位论文基于SPIN的UML活动图验证姓名：薛克申请学位级别：硕士专业：工程（软件）指导教师：刘静20080401论文摘要随着计算机技术的飞速发展，软件系统的广泛应用，软件系统问的可移植性、协同工作能力和可维护性问题R益突出，以模型为软件开发关键的模型驱动架构MDA方法是解决这些问题而产生的新技术。用UML活动图建立MDA中的平台无关模型PIM是模型的核心之一。但是很多模型在建模过程中缺乏正确性验证或仅进行局部的语法检验，造成模型存在死锁、活锁等缺陷，这直接引发了模型执行过程中的诸多问题，如任务不能完成、超期完成等。因

2、而，在建模阶段验证模型的正确性就显得尤为重要。在国家863项目“模型驱动式高可信软件开发技术"(编号：2006AA012165)的支持下，我作为小组成员实现了对UML活动图的自动化验证。模型检测作为形式化验证模型的方法，有着自动化和提供反例等诸多优点。并且近年在UML模型中得到广泛应用。模型检测器SPIN是由贝尔实验室开发的一种专门用于软件验证的工具。本文基于模型检测工具SPIN，对UML活动图建立的PIM模型进行形式化分析和验证，并对UML活动图进行动态模拟。首先在UML活动图建立的PIM模型基础上，将UML活动图转化为模型验证工具

3、SPIN能够识别的PROMELA语言模型，然后结合SPIN的验证功能对活动图进行验证，给出验证信息，并且在出错的情况下可以对活动图进行动态模拟。【关键词】：UML活动图，模型检测，SPIN，MDA，验证ABSTRACTW阶thedevelopmentofcomputertechnology,theextensiveapplicationofsoftwaresystem．theportability,serviceabilityandcooperationabilityofsoftwaresystembecomemoreandmorei

4、mportanLMDA(ModelDdvenArchitecture)whichtakethemodelasthekeyofsoftwaredeveloping，isanewtechnologytoresolvetheseproblems．PIM(PlatformIndependentModel)。whichissetupwithUMLactivitychartisoneoftheCOreofthemodel．ButmajorityoftheModelslackforverificationofcorrectionoronlychec

5、kthelocalexpressionsdunngthemodelingprocess，SOcausingtheexistenceofthedeadlock，live-lockandotherbugsinthemodel．Itcausesmanyproblemsdirectlydunngthedynamicexecutionofthemodel．Soitisimportantthatmodelandverifythemodelbeforerunning．onthesupportofNationalHigh-techR&DProgram

6、。Model-dnvenhigh—reliabilitysoftwaredevelopmenttechnology,1wasasateammembertoachievetheUMLactivitydiagramoftheautomatedverification．Modelchecking，asoneoftheformalmethodshasmanygoodadvantages，suchasautomatismandprovidingtheviolateexample．Recentyears，modelcheckinghasbeenp

7、opularinvenfyingUMLmodel．ModelcheckerSPINisdevelopedbyBellLabanditcanbeusedtoanalysisandverifysoftware．BasedonthemodelcheckerSPIN。thispaperisanalysisandverifythePIMmodelofUMLactivitychart．Firstly,onthebaseofPIMmodelsetupbyUMLactivitychart．coverttheUMLactivitychartintoPR

8、OMELAmodelwhichcanbeidentifiedbymodelchecktoolSPIN，thencombinetheverificationfunctionofSPINtocarryonaverificat