Verification Of Workflow Model Based On Petri Nets

The modeling of a workflow process is a complicated and error-prone procedure. However, the process verification in modeling phrase is comparatively weak at present. The cost will be very high if errors are found after the workflow is carried out in practice; therefore, the process verification is essential in the modeling of workflow phrase. Especially in recent years, with workflows plays a more and more important role in business process reengineering, there is an urgent demand for verification research and analysis of complex process. Therefore, to improve the model theory has become an important research direction.The dissertation tries to make contributions to the research of workflow verification; the research is focused on Petri Nets analysis theories. In order to demonstrate the theory the dissertation proposed, it is applied to a JBPM workflow management system.By studying many available researches on workflow verification and using the Petri theory on structural and behavioral properties, the dissertation analyses the good qualities and defects of the available achievements, and proposes an algorithm for the soundness of the workflow model according to the characteristics of Wfnet. JBOSS JBPM management system is introduced in Chapter 4 of the dissertation.JBPM is an open source and lightweight workflow management system. The most important feature of JBPM is JPDL; JPDL is a process language to implement BPM and workflow in java. An algorithm for mapping JPDL to Petri Nets is given on the basis of Alast's task structure and JPDL language, it will facilitate the use of Petri Nets in workflow model verification process.A JBPM instance is made in the end of the dissertation, the instance attempt to demonstrate the right and soundness of the theory proposed in chapter 3 and chapter 5 of the dissertation.