UML-statecharts Based Verification of Control Flow of the Workflow
基于UML-Statecharts的工作流控制结构的验证

Verification of workflow model has been one of the important research fields of workflow. The correctness of the control flow is the basic requirement that the workflow process must satisfy. In this paper, we emphasize on the verification of the control flow. We construct the control flow model by UML-Statecharts, and express that the property the control flow must satisfy by temporal logic. Then we give a theorem and prove it,also according to it give an algorithm of verification of soundness. For the verification of the property about workflow semantics we also give an algorithm.