基于uml的工作流模型自动分析验证研究--优秀毕业论文

《基于uml的工作流模型自动分析验证研究--优秀毕业论文》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

1、华南师范大学硕士学位论文基于UML的工作流模型自动分析验证研究姓名：谢洪萍申请学位级别：硕士专业：计算机软件与理论指导教师：苏开乐20050601华南师范大学硕士学位论文答辩合格证明学位申请人塑遨盏向本学位论文答辩委员会提交题为妻童幽圭垡圣堡盘盔鲤鱼亟筮堑量蛀壬邈亟的硕士论文，经答辩委员会审议，本论文答辩合格，特此证明。学位论文答辩委员会委员(签名)主席：鲍改豫避吻№色，论文指导老师(签名)：bR∈A}B摘要工作流是在计算机辅助下全部或部分自动执行的工作过程。Internet的发展对工作流的发展起了极大的促进作用，使计算机支持的分布

2、式、协同工作的工作流系统在企、事业单位中得到越来越多的应用。在现实世界中设计一个应用工作流是一个复杂而易出错的过程。缺少有效的方法和工具保证工作流的『F确性已成为工作流得到进一步广泛应用的一个障碍。模型检测(ModelChecking)是一种采用形式化方法的自动分析和验证技术，相对于传统形式化证明方法，具有快速、准确、全自动、对使用人员数学背景要求不高的特点，目前已在协议验证、分布式系统的设计和验证等方面得到成功的应用，为工作流模型验证提供了新的方法。本论文研究使用模型检测技术的工作流模型的验证方法。沦文首先介绍了工作流相关概念以及

3、模型检测技术的理论和方法，其中对模型检测工具Spin及其输入语言作了较详细的阐述。然后对工作流模型及其UML建模方法进行研究，提出基于UML的以模型检测为目的的工作流模型建模方法，并定义了模型的形式化描述；定义了工作流的形式化模型到Spin／Promela模型的转化规则，使用Spin对工作流模型的结构、语义正确性进行分析和验证。在前面工作的基础上设计了一个基于UML的工作流模型的自动分析和验证的工具，实现由工作流UML模型到Spin／Promela模型的自动转化，使不熟悉模型检测技术的工作者也能使用该方法对工作流进行验证。关键字：工

4、作流：UML；模型检测；Spin第1负Abs仃aclAbstractWorkflowisabusinessprocessexecutingcompletelyorpartiallyautomaticallywiththeaidofcomputer．ThedevelopmentofIntemethasgreatlypromotedthedevelopmentofworkflowinthepasttwentyyears．Computersupportedcooperationanddistributedworkflowsystemsal

5、ebecomingmoreandmorewidelyusedingovernmentsandenterprises．Yetinrealisticworld，designinganapplicationworkflowisacomplexandfallibleprocess．Lackofeffectivemeansandtoolshasbeenoneoftheobstaclesforworkflowtobefurtherandmorewidelyused．ModelCheckingisanautomaticanalysisandver

6、ificationtechnologyusingformalmethods．Comparedwithtraditionalformalmethods，itisfast，completelyautomaticanddoesnotrequirestrongmathematicbackground．Presentlymodelcheckinghasbeensuccessfullyappliedinseveralfieldssuchasprotocolverification，designandverificationofdistribut

7、edsystem．Itprovidesanewmethodforworkflowverification．Thispaperfocusesontheverificationmethodsofworkflowmodelbasedonmodelchecking．Itfirstlyintroducesrelativeconceptionsaboutworkflowandthetheoriesandmethodsofmodelchecking，mainlydescribingtheworkofmodelcheckingtoolSpinand

8、itsmodellanguagePromela．BasedonthestudyofthecharacterofworkflowmodelandmodellingmethodsusingUML，itputsforwardamodelli