工作流模型时间有界性验证与分析研究

Timing Boundedness Verification and Analysis of Workflow Model

对工作流模型分析进行了层次划分后 ,提出了工作流模型时间有界性的问题。从完成工作流管理联盟给出的工作流图形化模型向工作流网的模型映射之后 ,利用绝大多数描述业务过程的工作流模型都具有自由选择特性的特点 ,提出了一种将映射得到的自由选择工作流网分解为一组变迁组件网的分解算法。在此基础上 ,结合工作流模型的资源视图 ,详细阐述了基于Petri网理论的工作流模型时间有界性分析与验证方法。

The analysis of a workflow model is classified into logic, temporal, and performance levels. To avoid the run-time congestion of a workflow model, the problem of timing boundedness verification of a workflow model is put forward. We extend the WorkFlow nets (WF-nets) with resource and time information as the Multi-Dimension WorkFlow nets (MDWF-nets), then the model mapping from a workflow model built by the WfMC's graphic process modeling language to the MDWF-nets is discussed in detail. According to the free-choice characteristics of workflow model for business process, an algorithm for decomposing a free-choice MDWF-nets based workflow model into a set of T-component is proposed. Then, taking into account the resource view of a workflow model, the method of verifying the timing boundedness of a workflow model is given.