基于UML-Statecharts的工作流控制结构的验证

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.