工作流模型的模型检验技术研究.pdf

《工作流模型的模型检验技术研究.pdf》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

1、第22卷第ll期计算机仿真2005年ll月文章编号：l006-9348（2005）ll-0073-05工作流模型的模型检验技术研究汪文元，沙基昌（国防科学技术大学信息系统与管理学院，湖南长沙4l0073）摘要：传统的工作流模型校核方法存在效率低下、自动化程度不高的缺陷，针对该问题模型检验技术被引入工作流模型校核。该文在探讨模型检验技术基础之上，采用UML活动图表示工作流过程模型，根据模型检验技术的要求研究了工作流模型从无限到有限状态空间的转换，对工作流模型检验对强公正约束的要求进行了初步研究，并结合NuSMV分析了如何实施工作流模型检验。该文进一步通过

2、一个案例给出了工作流模型检验的实施，在此基础上该文认为模型检验有助于提高模型校核效率，从而提高工作流模型质量。关键词：工作流；模型检验；状态空间转换；强公正约束中图分类号：TP3ll文献标识码：AResearchonModelCheckingTechnologyofWorkflowModelWANGWen-yuan，SHAJi-cang（CoIIegeofInformationSystemandManagement，NationaIUniversityofDefenseTechnoIogy，ChangshaHunan4l0073，China）ABSTR

3、ACT：ThetraditionaIworkfIowmodeIverifyingmethodsareinefficientandhaveIowerautomation.Inthepa-perthemodeIcheckingtechnoIogyhasbeenintroducedintoworkfIowmodeIverifying.BasedontheanaIysisofmodeIcheckingtechnoIogy，UMLactivitydiagramshavebeenusedtomodeIworkfIowprocesses.InordertoimpIe

4、mentmodeIchecking，weresearchedthetransitionfrominfinitestatespacetofiniteoneandthestrongfairnessconstraint.WeanaIyzedhowtoimpIementmodeIcheckingwithNuSMV.AndthenanexampIewasgiventoshowthepracticabiI-ity.FinaIIythepaperconcIudedthatthemodeIcheckingtechnoIogycanbeusedtoimproveveri

5、fyingefficiency，andthenthemodeIguaIitycanbeimproved.KEYWORDS：WorkfIow；ModeIchecking；Statespacetransition；Strongfairnessconstraint1引言并发系统的模态/命题性质。分为基于自动机理论的模型检［2］［5］工作流模型是工作流应用的生命线，模型的可用性直接验和符号模型检验两个派别。模型检验与其它验证技受模型质量的影响，因此对于如何确保模型质量研究一直是术或者方法相比有许多优点，最重要的就是高度自动化。工作流工作者十分关注的问题。总体来

6、讲这方面的工作可［1，4］概括为工作流模型的VVSA，本文主要关注第一个V（即校2模型检验基础核）。其中由于工作流模型的复杂性，使得工作流模型很可2.1计算树逻辑能不能正确反映建模人员的建模意图，甚至存在错误，这就命题时态逻辑是一种依赖于时间的命题逻辑，分为线性需要校核。传统的校核方法，如Petri网方法，自动化程度很时态逻辑（IineartimeIogics，LTL）和分支时态逻辑（branch低，对建模人员要求很高，并且对建模方法要求甚高，导致工timeIogics，BTL），计算树逻辑（ComputationTreeLogics，作流模型的校核效

7、率低下，从而影响模型质量并进一步影响CTL）将这两种时态逻辑操作符组合在一起。线性时间操作其可用性。符有X（neXt）、U（UntiI）、F（sometimes，Future）和G（aIways，模型检验（modeIchecking）是多种形式化校核技术的一GIobaI），而路径标识A（forAIIpaths）和E（forsomepaths，［l］Exists）则均可用于线性时间操作符之前用于对其的修饰。种，可自动化进行有限状态空间响应性系统校核，于l98l年由CIark和AIIenEmerson以及OuieIIe和Sifakis分别提出。在CTL中存

8、在两类范式，即状态范式和路径范式。状态范式主要通过线式状态搜索或隐式不动点计算来验证有穷状态是