一种基于扩展UML状态图的并发工作流验证方法

摘要

当并发执行工作流的多个实例时会导致数据流访问时语义的不一致。首先扩展了传统的UML状态图，用它进行工作流实例建模。然后把扩展的UML状态图建立的工作流模型转化为Biichi自动机，并用Biichi自动机之间的积表示多个工作流实例的并发模型。接着给出了和证明了根据并发模型中标记的命题公式判定并发冲突的定理。最后，由于随着实例数目的增加，并发模型中的状态数也会按每个实例的状态数倍增加，为了解决这一问题，在检测并发冲突的算法中采用了on—the—fly技术.