基于层次时间Petri网的工作流模型可达性分析方法

为了有效管理工作流,需要对工作流模型进行合理性分析与验证.为此,提出了一种基于层次时间Petri网的工作流模型,给出了从时间Petri网工作流模型转化成基于层次时间Petri网工作流模型的规则及算法.证明了任何一个能够转化成基于层次时间Petri网的时间Petri网工作流模型在物理上都是可达的.在时间方面,提出了基于层次时间Petri网工作流模型的层次时间树算法,并给出了时间可达性的静态和动态分析与验证方法.通过实例验证了该方法在工作流模型的物理、时间静态和时间动态可达性分析中的有效性.

Method of reachability analysis in HTPN based workflow model

The rationality analysis and verification of workflow are crucial to the effective management and execution of it.A new temporal workflow model based on Hierarchically Timed Petri Net(HTPN) was proposed to implement the analysis and verification of Timed Petri Net(TPN) workflow model.The rules and algorithm of transforming TPN model into HTPN model were given.And it was proved that a workflow model based on TPN would be physically reachable if the model was able to be transformed into a HTPN model.A new algorithm,HTPN based Hierarchically Timed Tree(HTT),was presented to implement the analysis and verification of static and dynamic availability.Finally,a case study was used to illustrate the effectiveness of above-mentioned method in the analysis and verification of static and dynamic availability in a workflow model.