Performance Analysis And Formal Verification Of Workflow Model: An Extended Petri-Net-Based Approach

Performance analysis and process verification of workflow model is one of the most important aspects on the research and application of workflow system. According to Petri Net's shortage that modeling scale enormously, limitation of its description function and no characteristic of hiberarchy, this dissertation proposes an Extended Hierarchical Colored Petri Net (EHCPN) approach to simulate and verify the process of workflow model, which remedy shortage of Petri Net. EHCPN model is object-oriented, which is comprehensive and improve efficiency of modeling and analysis of workflow model.This dissertation places emphasis on the modeling, simulating and verification of workflow model. Firstly, we formalize EHCPN model, and give a rule which transform from workflow meta-model to workflow EHCPN model. Based on workflow EHCPN model, we design and implement a suite of tools, WF-P/TMSE, which model, simulate and verify workflow. On the part of verification, we propose a state group construction algorithm, which can construct state spaces needed by verification quite efficiently. At last, we create corresponding EHCPN model in WF-P/TMSE through some cases of workflow process model, which is simulated and verified, and give the data and results of simulating and verification separately.The results of simulating and verification show that favorable Mathematical Definition and powerful description capability of EHCPN model can express workflow's structural characteristics correctly, EHCPN-based WF-P/TMSE can support all the process of modeling, simulating and verifying workflow, and state class construction algorithm can construct the state spaces of workflow EHCPN model efficiently, and improve efficiency of workflow EHCPN model verification.