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

工作流模型验证成为工作流的重要研究领域之一。控制结构的正确性是工作流过程所需达到的最基本要求,本文着重控制结构方面的验证。本文使用 UML-Statecharts 建立控制结构模型,使用时序逻辑表示工作流控制结构需要满足的性质。给出了一个定理并进行了证明,基于定理给出了一个验证完全性的算法,对于工作流语义相关性质的验证给出了一模型检测算法。