工作流图结构冲突识别与图约简技术应用

### 工作流图结构冲突识别与图约简技术应用 #### 1. 过程模型中的结构冲突 在过程模型中，存在两种结构冲突：死锁和缺乏同步。所有在初始节点后引入的拆分结构，都要在到达最终节点前通过合并结构闭合。具体来说，“与 - 合并”用于合并“与 - 拆分”路径，“或 - 合并”用于合并“或 - 拆分”路径。 - **死锁冲突**：用“与 - 合并”来合并排他的“或 - 拆分”路径会导致死锁冲突。在“与 - 合并”处发生死锁时，由于“与 - 合并”的一个或多个前置流未被触发，工作流路径的继续执行会被阻塞。 - **缺乏同步冲突**：用“或 - 合并”来合并“与 - 拆分”的并发路径会引入缺乏同步冲突。“或 - 合并”节点处缺乏同步会导致“或 - 合并”节点后续的节点被意外多次激活。 结构冲突并非过程模型中唯一可能出现的错误类型，但它们是控制流规范中错误的主要来源。其他建模方面也可能影响工作流的正确执行，例如： - **数据流建模**：捕获活动之间的数据依赖关系。由于建模不正确，依赖活动在运行时可能无法从源活动获取所需数据。 - **数据映射**：活动与底层应用组件之间的错误数据映射也可能导致工作流执行不正确。 - **时间约束**：工作流模型的控制流规范可能不满足某些指定的时间约束。 工作流模型中其他错误的存在不会引入或消除结构冲突，因此工作流模型中结构冲突的识别可以独立于其他类型的验证分析进行。仅从工作流图中移除结构冲突并不能保证完整工作流规范的正确性，但工作流模型中不存在结构冲突可保证控制流规范符合一定的正确性标准。 #### 2. 工作流结构验证过程 工作流结构的验证过程分为两个阶段： 1. **基本语法检查阶段**：确保模型符合建模语言的语法，并且其组件的所有必要属性都已定义。此阶段的验证易于实施，只需对工作流建模对象和结构进行局部分析。例如，检查工作流模型是否为有向无环图（DAG）以及是否正确连接。 2. **严格分析阶段**：对工作流模型进行严格分析，尝试识别由于建模结构的冲突使用而可能出现的不一致性。这些冲突结构可能位于工作流图的不同位置，手动识别这些不一致性较为困难。 在介绍工作流图的正确性标准之前，需要定义实例子图的概念。实例子图表示工作流特定实例可能执行的工作流任务的子集。它可以通过基于底层建模结构的语义访问其节点来生成。表示已访问节点和流的子图构成实例子图。 工作流图的正确性标准如下： - **无死锁工作流图**：如果工作流图不会生成仅包含“与 - 合并”节点的部分入边节点的实例子图，则该工作流图无死锁结构冲突。 - **无缺乏同步工作流图**：如果工作流图不会生成包含“或 - 合并”节点的多个入边节点的实例子图，则该工作流图无缺乏同步结构冲突。 验证这两种情况的共同点是，原则上需要检查工作流的所有可能实例子图。“或 - 拆分”是工作流图中唯一会引入多个可能实例子图的结构。没有“或 - 拆分”结构的工作流图将生成与工作流图完全相同的实例子图。具有单个“或 - 拆分”结构的工作流图生成的可能实例子图数量与“或 - 拆分”结构的出边流数量相同。然而，随着工作流规范中“或 - 拆分”和“或 - 合并”结构数量的增加，可能的实例子图数量会呈指数级增长。因此，使用蛮力方法生成工作流图的所有可能实例子图来确保正确性在计算上是低效的。 #### 3. 工作流图的形式化表示 工作流图 $G = ( N, F )$ 是一个简单的有向无环图（DAG），其中： - $N$ 是有限的节点集。 - $F$ 是有限的控制流集，表示两个节点之间的有向边。 对于每个流 $f \in F$： - $head[f] = n$，其中 $n \in N$ 表示 $f$ 的头节点。 - $tail[f] = n$，其中 $n \in N$ 表示 $f$ 的尾节点。 对于每个节点 $n \in N$： - $type[n] \in \{ TASK, CONDITION \}$ 表示 $n$ 的类型。 - $dout[n]$ 是 $n$ 的出度，即从 $n$ 发出的流的数量。 - $din[n]$ 是 $n$ 的入度，即流入 $n$ 的流的数量。 - $Outflow[n] = \{ f : f \in F \text{ 且 } head[f] = n \}$，即从 $n$ 发出的流的集合。 - $Inflow[n] = \{ f : f \in F \text{ 且 } tail[f] = n \}$，即流入 $n$ 的流的集合。 - $Outnode[n] = \{ m : m \in N \text{ 且 } \exists f \in F \text{ 使得 } head[f] = n \text{ 且 } tail[f] = m \}$，即与 $n$ 相邻的后续节点的集合。 - $Innode[n] = \{ m : m \in N \text{ 且 } \exists f \in F \text{ 使得 } tail[f] = n \text{ 且 } head[f] = m \}$，即与 $n$ 相邻的前置节点的集合。 图 $G$ 满足以下语法正确性属性： - 条件节点不用于顺序结构，即 $\neg\exists n \in N$ 使得 $type[n] = CONDITION$ 且 $din[n] \leq 1$ 且 $dout[n] \leq 1$。 - $G$ 不包含多个初始节点，即 $\exists n \in N$ 使得 $din[n] = 0$ 且 $\neg\exists m \in N$ 使得 $din[m] = 0$ 且 $n \neq m$。 - $G$ 不包含多个最终节点，即 $\exists n \in N$ 使得 $dout[n] = 0$ 且 $\neg\exists m \in N$ 使得 $dout[m] = 0$ 且 $n \neq m$。 #### 4. 约简规则 验证方法和算法的基本思想是从工作流图中移除那些肯定正确的结构，这通过迭代应用保留冲突的约简过程来实现。该约简过程最终会将结构正确的工作流图约简为空图，而存在结构冲突的工作流图则不会被完全约简。约简过程使用三种约简规则：相邻约简规则、闭合约简规则和重叠约简规则，只要它们能够对图进行约简就会被使用。 - **相邻约简规则**：该规则针对四种类型的组件。遍历图的所有节点，检查应用相邻约简规则是否可以对其中任何节点进行约简。 - 如果当前节点连接的流的数量小于或等于 1，则将其从图中移除。同时，当一个节点从图中移除时，所有连接到它的流会自动被移除。 - 如果当前节点形成顺序结构（即它恰好有一个入边流和一个出边流），则将其入边流的尾节点改为其出边流的尾节点，并将其从图中移除。 - 如果当前节点未通过前两个条件被移除，说明它正在形成拆分或合并结构（因为它的出度或入度或两者都大于 1）。若当前节点有单个入边流且通过多个出边流引入拆分结构，并且当前节点的类型与其前置节点相同，则将当前节点的出边流移动到前置节点，并移除当前节点。 - 若上述条件都不满足，检查当前节点是否有单个出边流且通过多个入边流引入合并结构。如果当前节点的类型与其后续节点相同，则将当前节点的入边流移动到后续节点，并删除当前节点。 - **闭合约简规则**：相邻约简规则的应用通常会在工作流图中引入闭合组件。闭合组件由两个相同类型的节点组成，它们之间有多个流。闭合约简规则会删除这些节点之间除一个流之外的所有流。 - **重叠约简规则**：重叠约简规则针对工作流图中出现频率较低的特定类型组件。只有当相邻约简规则和闭合约简规则无法对图进行约简时，才会调用该规则。重叠组件具有四个层次，其源节点（第 1 层）始终是条件节点，汇节点（第 4 层）始终是任务节点。第 2 层只有任务对象，第 3 层只有条件对象。第 2 层的每个任务都有到第 3 层每个条件的出边流，并且从第 1 层的源节点恰好有一个入边流。第 3 层的每个条件只有来自第 2 层每个任务的入边流，并且到第 4 层的汇节点恰好有一个出边流。第 3 层和第 4 层的节点除上述流外没有其他控制流连接。重叠约简规则会识别满足所有这些属性的组件，并将其约简为组件源节点和汇节点之间的单个控制流。 工作流图在约简前假定满足前面所述的语法正确性属性，但在约简过程中，约简后的图可能不满足某些属性。相邻约简可能会在两个节点之间引入多个流，从而将简单图转换为多重图；闭合约简和重叠约简可能会引入顺序条件节点。在约简后的工作流图中，允许存在这两种语法错误。 #### 5. 验证算法 三种约简规则被组合到以下的 `REDUCE(G)` 算法中，该算法以工作流图 $G$ 作为输入： ```plaintext procedure ```