Page 177 - 《软件学报》2020年第10期

莫启 等:协同业务过程的建模及正确性修正 3153

的,进而可推出其中含有的简单路径数量及长度也是有穷的.
1 a
n a
定义 11(完整的简单路径). 设σ=c 0 ⎯⎯→ c 1 …c n−1 ⎯⎯→ c n 为协同业务过程 CBP 中的一条简单路径,称σ为
完整简单路径,当且仅当 c n 为终止格局.
特别地,完整的简单路径所对应的轨迹称为完整轨迹.由弱合理及简单路径,对协同业务过程进行合理性分
析可转换为对简单路径的分析,见定理 1.
定理 1. 设 R 为协同业务过程 CBP 中所有的简单路径集合,若对于任意简单路径 r∈R,r 是完整简单路径,
则 CBP 是弱合理的.
a
1 a
证明:设 c m 为从 c 0 出发且经迹σ到达的任意一个格局,则可推出存在路径 r=c 0 ⎯⎯→ c 1 …c m−1 ⎯⎯→ c m ,满足
m
trace(r)=σ,分下面两种情况加以讨论.
σ
t
1) 若 c m 为终止格局,则推出存在空迹 t,使得 c m ⎯⎯→ c e ,即 c 0 ⎯⎯→ c e .
2) 若 c m 为非终止格局,再分下面两种情况加以讨论.
(1) 若 r 满足∀1≤i,j≤m∧j≠i,c i ≠c j ,则可知 r 为某条简单路径 r a ∈R 的前缀片段.由于 r s 是完整路径,则可知必
σ
t
^t
定存在迹 t,使得 c m ⎯⎯→ c e ,即 c m ⎯⎯⎯→ c e .
k a
(2) 若 r 存在片段 c i ⎯⎯⎯→ c i+1 …c j …c k−1 ⎯⎯→ c k (1≤i,j,k≤m),满足 c i =c j =c k ∧∀i<x,y<k∧x≠{i,j,k}∧y≠{i,j,k}
1
i a +
j a
∧x≠y,c x ≠c y ,可知轨迹 r 中存在重复次数大于 2 的循环结构,则在 r 中使用 c i 替换掉片段 c i ⎯⎯⎯→ c i+1 … ⎯⎯→ c j .
1
i a +
反复执行循环结构替换操作,最终得到替换后的 r′必定为简单路径,则可知 r′为某条简单路径 r s ∈R 的前缀片段.
σ
t
^t
由于 r s 是完整路径,则可知必定存在迹 t,使得 c m ⎯⎯→ c e ,即 c 0 ⎯⎯⎯→ c e .
综合上述(1)和(2)及定义 9,结论成立.证毕. □
基于定理 1,设 R 为协同业务过程 CBP 中所有的简单路径集合,R 中所有的完整简单路径为 R c .若|R c |=0,表
示 R 中每条简单路径均不是完整路径,则称 CBP 是完全不正确的;若|R c |≠0∧|R c |<|R|,表示 R 中有部分简单路径是
完整简单路径,则称 CBP 是部分正确的;若|R c |=|R|,表示 R 中所有的简单路径均是完整路径.根据定理 1 可知,CBP
满足弱合理性,称 CBP 是完全正确的.
只有在部分正确的情况下,才可能且有必要对协同业务过程进行修正.以获得的所有完整简单路径为基础,
下面详细地阐述针对协同业务过程的修正方法.
4 正确性修正
针对部分正确的协同业务过程,其修正可分 3 步进行:(1) 将所有完整的简单路径合并为核;(2) 将核映射为
修正业务过程;(3) 将产生的修正业务过程利用并发操作符组合,构建修正协同业务过程.
对于部分正确的协同业务过程而言,根据第 3 节中的阐述可知,其中必定含有完整的简单路径(即能够正确
地执行完成路径)和非完整的简单路径(即导致协同业务过程执行失败路径).为了捕获其中含有的所有正确路
径(即完整的简单路径),本文提出了核的概念.本质上,对于一个部分正确的协同业务过程,它对应的核是含有其
中所有完整简单路径的一个迁移系统.
定义 12(核). 核是五元组 c=(C,c 0 ,C e ,A,Δ),其中,
(1) C 为格局集合;
(2) c 0 ∈C 为初始格局;
(3) C e ∈C 为终止格局集;
(4) A 为活动集合;
(5) Δ∈C×A×C 为格局迁移关系集合.
1 a
n a
特别地,对于任意核 c,其行为也可由路径表示.对于 c 中任意路径 r=c 0 ⎯⎯→ c 1 …c n-1 ⎯⎯→ c n …,满足∀i∈
i a
[1..n],c i−1 ⎯⎯→ c i ,当且仅当(c i−1 ,a i ,c i )∈Δ.
下面提出算法 2,用来将所有完整的简单路径合并以构建核.