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

传统的工作流模型校核方法存在效率低下、自动化程度不高的缺陷,针对该问题模型检验技术被引入工作流模型校核.该文在探讨模型检验技术基础之上,采用UML活动图表示工作流过程模型,根据模型检验技术的要求研究了工作流模型从无限到有限状态空间的转换,对工作流模型检验对强公正约束的要求进行了初步研究,并结合NuSMV分析了如何实施工作流模型检验.该文进一步通过一个案例给出了工作流模型检验的实施,在此基础上该文认为模型检验有助于提高模型校核效率,从而提高工作流模型质量.

Research on Model Checking Technology of Workflow Model

The traditional workflow model verifying methods are inefficient and have lower automation.In the paper the model checking technology has been introduced into workflow model verifying.Based on the analysis of model checking technology,UML activity diagrams have been used to model workflow processes.In order to implement model checking,we researched the transition from infinite state space to finite one and the strong fairness constraint.We analyzed how to implement model checking with NuSMV.And then an example was given to show the practicability. Finally the paper concluded that the model checking technology can be used to improve verifying efficiency,and then the model quality can be improved.