Workflow Verification Based On XPFL-Research & Implementation Of Flow LyzerXP

More and More people are concentrating on workflow verification. However, few are very successful. This dissertation is trying to proceed a better approach.FlowSxp is a Workflow Management System supporting discrete schedule and strong workflow verification, which extremely satisfies the requirement of inter-enterprise business cooperation. FlowLyzerXP is a sub-system of FlowSXP. Based on that, this dissertation put forward a deep and complete discussion about the structural verification of workflow. Moreover, most content of this dissertation is applied and proved to be correct in FlowLyzerXP system.In the 1st chapter, we introduce workflow and workflow verification briefly to make the readers understand the development and application of workflow technology and some relevant concepts. We also explain why verification is necessary for workflow application and summarize the criterion of workflow verification. Then, we bring out our definition of workflow verification and enumerate some research interesting about workflow verification at last.In the 2nd chapter, we bring out a workflow language based on XML and Petri Net-XPFL , and a meta-model based on XPFL. Firstly, we introduce this language briefly. Then, the detail of XPFlL's process model is explained, including process model, task and transition. Based on that, the rules of soundness, which includes dead task, option to complete and proper completion, are discussed.In the 3rd chapter, we discuss the algorithmic models. Firstly, we bring out a extended Petri Net-WFXP Net and explain how to diagnose dead tasks and the option to complete in a workflow process. Then, based on WFXp net, the CAR Net is introduced, which is used to avoid deadlocks and livelocks. Last, we discuss the diagnosis of deadlock and synchronization using Pair Net. This chapter is the algorithmic basis of workflow verification.In the 4th chapter, we introduce the implementation of workflow verification based on XPFL, meta-model and algorithmic models. Firstly the abstract and predigestion of XPFL is discussed. Then . we explain the transition from XPFL model to all algorithmic models. Last a verification process is putted forward. This chapter is the implementation basis of FlowLyzerXP .In the 5th chapter, we explain the implementation of FlowLyzerXP system. After introducing the architecture of FlowSxp and FlowLyzerXp, we explain the XPFL meta-model and algorithmic models ulteriorly by studying a "Customer Complaint Process" case.In the end, all of the works in this dissertation are summed up, and their futures are prospected.