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

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

足弱轨迹等价,则最小化隐藏核后生成的业务过程 BP 中有如下迁移,记为 C2:
A
s ⎧ ⎪ i =s i− 1 , a ∉∪ A c
i
c i− 1 ⎯⎯→ i a c = i ⎨ .
s ⎪ ⎩ i− 1 ⎯⎯→ i a i , s a ∈ i A∪ A c
根据定义 15,每个修正业务过程 BP rj (1≤j≤n)中的迁移进行如下协调映射,记为 C3:
s ⎧ i =s i− 1 , a ∉ i A a∧ i ∉ A c
⎪ ⎯⎯→ i a a ∈ A a ∉ ∧
c i− 1 ⎯⎯→ i a c = i ⎪ ⎨ s i− 1 i , s i i A c .
SYNC _1_ a
⎪ s i− 1 ⎯⎯⎯⎯⎯→ s ⎯ 1 c ⎯ i a → s ⎯⎯⎯⎯⎯→ SYNC _ 2 _ a s i , a ∈ i A a ∈ ∧ i A c
2
c
⎪ SYNC _1_ a SYNC _ 2 _ a
⎩ s i− 1 ⎯⎯⎯⎯⎯→ s ⎯ c ⎯ ⎯ ⎯ ⎯ → i , s a ∉ i A a ∈ ∧ i A c
从左至右依次扫描 r,根据定义 5 中的点火规则可生成如下路径 r′,满足:
i a
SYNC_2_ i a
SYNC_1_ i a
r′=k 0 …k i−1 ⎯⎯⎯⎯⎯→ k (i−1)i1 ⎯⎯→ k (i−1)i2 ⎯⎯⎯⎯⎯→ k i …k m (a i ∈A c ),
i a
或 r′=k 0 …k i−1 ⎯⎯→ k i …k m (a i ∉A c ).
根据 C3,由于 r 为完整的简单路径,则可推出 r′中 k m 也为终止格局,故 r′是完整的简单路径.进一步地,推出
trace(r)=trace(r′)↑A cf 成立.根据定理 2,c 与 CBP 中完整的简单路径一致,故结论(1)成立.
1 a
k a
2) 采用反证法证明.设 CBP r 中存在路径片段 r 1 =k 0 ⎯⎯→ k 1 …k k−1 ⎯⎯→ k k ,且 c 中存在对应路径片段 r 2 ,满
a
1 a
k a
足 trace(r 2 )=trace(r 1 )↑A cf .但 CBP r 中存在后续迁移 k k ⎯⎯→ k k+1 使得路径片段 r 3 =k 0 ⎯⎯→ k 1 …k k−1 ⎯⎯→
a
k k ⎯⎯→ k k+1 不为 c 中任意完整的简单路径的前缀.按如下两步证明后续活动 a 不能发生.
(1) 首先明确活动 a 是协调活动,即 a∈A c .针对路径片段 r 1 ,由于 c 中存在对应路径片段 r 2 ,满足 trace(r 2 )=
SYNC_1_ i a i a SYNC_2_ i a
trace(r 1 )↑A cf .因此,从左至右扫描 r 1 ,对于 r 1 中路径片段:k i−1 ⎯⎯⎯⎯⎯→ k c1 ⎯⎯→ k c2 ⎯⎯⎯⎯⎯→ k i ,或者 k i−1
a
i a
i a
⎯⎯→ k i ,则用 c i−1 ⎯⎯→ c i 替换,重复这一过程,最终可求得 k k 对应于 c k .由 C3 可知,若后续迁移 k k ⎯⎯→ k k+1 发生
后使得 r 3 不为 c 中任意完整简单路径的前缀,那么 a∈A c .
(2) 再证明协调活动 a 在 CBP r 中不能发生.分下面两种情况加以讨论.
a
i) a 不在 c 中出现,即 a∉c.A.由 C3 可知,后续迁移 k k ⎯⎯→ k k+1 不存在;
b
1 a
b
k a
ii) a 在 c 中出现,即 a∈c.A.设有后续有效迁移 k k ⎯⎯→ k k+1 ,使得 r 4 =k 0 ⎯⎯→ k 1 …k k−1 ⎯⎯→ k k ⎯⎯→ k k+1 为 c
中某条完整简单路径的前缀.若活动 a 能执行,再分如下两种情况进行讨论.
① 若 a 和 b 属于同一个修正业务过程 BP rj (1≤j≤n),则推出 a 和 b 处于选择关系.由 C3 可知,若 a 能够执
b
行,则 b 不能执行.但迁移 k k ⎯⎯→ k k+1 是有效的,故活动 a 不能执行;
② 若 a 和 b 属于不同的修正业务过程,不妨设分别属于业务过程 BP ri 和 BP rj (1≤i,j≤n).根据 C3 可推
a
SYNC_2_ a
b
SYNC_1_ a
出,BP rj 中存在迁移 s j ⎯⎯→ s j+2 ,s j ⎯⎯⎯⎯⎯→ s c1 ⎯⎯→ s c2 ⎯⎯⎯⎯⎯→ s j+1 .根据定义 5 给出的点火规则,
b
若活动 a 能够执行,则活动 b 不能执行.但迁移 k k ⎯⎯→ k k+1 是有效的,故活动 a 不能执行.
综合上述(1)和(2)推导可知,结论(2)成立. □
定理 3 中的结论(1)表明修正前的协同业务过程中所有完整的简单路径都可以在修正协同业务过程中重
现;而结论(2)则表明未引入隐藏轨迹.这将避免修正后进行有效性确认,从而提高了修正效率.
特别需要明确的是,本文方法可支持带有一般循环结构的过程模型,其原因在于修正是基于完整简单路径
开展.完整简单路径能够记录循环结构(即自循环和一般循环结构 [17] ),故通过算法 2 构建的核中循环结构也不
会丢失.最终,通过对核进行协调映射产生修正业务过程也含有已有环结构.
5 实验评价
本文提出一种协同业务过程正确性修正方法.为了评估该方法的有效性,本节使用具有实际意义的协同业
务过程集,通过与相关正确性修正方法进行实验对比,从修正协同业务过程具有协同业务过程实际特征、重现
完整轨迹及未引入隐藏轨迹等方面来分析不同正确性修正方法之间的有效性差异.