| As the explicit representation of the business process logic, the correctness of workflow process model determines whether can gain the business goal or not. The main purpose of verification in workflow modeling is to examine the discrepancy between the initial business goal and the result of the system. Management concept, such as business process reengineering and process improvement, makes enterprise focus on the business process. It is essential to detect all the potential errors of a workflow process definition before it becomes operational to reduce the cost of shutdown, inspection and modification of process during the run-time. As a result, the verification in workflow modeling is becoming more and more important as an essential part of workflow management.Compared with other formal methods, Petri net technology has both formal semantics and graphical nature, which can provide normative guidance and intuitive for designers. With state explicitly modeling capabilities and a wealth of analytical techniques, Petri net can not only reflect the real semantic of business process but also detect the structural correctness of the process model.As a modeling technology based on Petri net, Workflow net brings more structural and behavioral restrictions. Based on the research and summary of analysis techniques of Workflow net, the paper presents a verification model which is suitable for free-choice or well-structuredness Workflow net.In order to apply the verification model to the document flow system based on JBPM workflow engine, the paper discusses differences between models based on JBPM and workflow net. And then, an algorithm for mapping JBPM to Workflow net is given.Finally, the document flow system integrated with the approach proposed by the paper can detect structural errors, such as no start place, no end place, dead-locks, live-locks and dead transitions, of process model at design-time. The test result verifies that approach proposed by the paper is reasonable and useful in practice. |
