A method to verify the soundness of workflow control logic

Verification of workflow soundness is an important problem in the current workflow research area, but this problem has not been solved well. Many WfMSs probably create wrong workflow models, so the running of workflow will be abnormal. Theorem of event balance is introduced in Reference 3. A necessary condition to verify workflow logical soundness is proposed by analyzing the soundness of local workflow. But how to verify the soundness of a whole workflow is not introduced. In this paper, a workflow model based on a double-road conditional directed graph is created and a method to verify the soundness of a whole workflow is proposed. The experiential results prove that the method is feasible.