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

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

η.反复执行循环结构替换操作,最终得到替换后的 r′ c 必定为简单路径,推出 r′ c ∈R c .由算法 2 可知,由 R c 构建后的
c 中必定存在格局迁移关系集合{(c i ,a i+1 ,c i+1 ),…,(c j−1 ,a j ,c i )}⊆Δ,由此可生成任意重复次数(设为 p,p≥0)的循环片
段,即η p .由定义 9 可知,轨迹 r c 的长度有穷,可推出 r′ c 中的循环片段η的重复次数是确定整数(设为 q),即η q .由于
q≤p,可推出η q 可由 c 中格局迁移关系{(c i ,a i+1 ,c i+1 ),…,(c j−1 ,a j ,c i )}⊆Δ生成.同时,对于 r′ c 中任意非循环结构片段,
g a
g a
即 c g−1 ⎯⎯→ c g (1≤g≤n),不存在 c u ,c v (1≤u,v≤n∧u<g−1∧v>g),使得 c u =c v ,r′ c 中存在 c g−1 ⎯⎯→ c g ,由算法 2 可知,
g a
g a
(c g−1 ,a g ,c g )∈Δ.因此,从左至右扫描 r c ,对于非循环结构路径片段 c g−1 ⎯⎯→ c g ,r′ c 中存在 c g−1 ⎯⎯→ c g ,则可推出其
j a
i a +
i a +
可由 c 中(c g−1 ,a g ,c g )∈Δ生成,而对于多次重复的循环结构η k (η=c i ⎯⎯⎯→ c i+1 … ⎯⎯→ S i ),r′ c 中存在 c i ⎯⎯⎯→
1
1
j a
c i+1 … ⎯⎯→ c i ,则可推出其可由{(c i ,a i+1 ,c i+1 ),…,(c j−1 ,a j ,c i )}⊆Δ生成,重复这一过程,最终可由 c 生成 r c .
必要性.可按类似方式证明,限于篇幅,这里从略. □
给定部分正确协同业务过程 CBP=BP 1 ||BP 2 ||…||BP n ,根据算法 2 生成的 CBP 的核为 c.本文中,对 CBP 进行
修正目标是要保证 CBP 中完整简单路径对应轨迹可在修正后的协同业务过程 CBP r =BP r1 ||BP r2 ||…||BP rn 中重
现,且 CBP r 中仅含有这些完整简单路径的轨迹,以避免后续有效性确认,提高修正效率.其中,BP r1 ,…,BP rn 分别为
业务过程 BP 1 ,…,BP n 对应的修正业务过程.根据定理 2,这一问题可转换为保证 CBP r 和核 c 的行为一致.
为了生成与 CBP 行为一致的 CBP r ,基于核 c,本文提出协调映射概念.协调映射是指在映射过程中引入协调
因子(对应活动),用于建模协调交互以实现协调逻辑,从而确保由映射生成 BP r1 ,…,BP rn 并发组合形成 CBP r 能够
遵循 cc 行为.从外界视角来观察,在忽视协调因子的情况下,协调映射可使得 CBP r 只包含 CBP 中所有完整简单
路径的轨迹.
在实际应用中,不是 CBP 中的每个活动都需要进行协调.以核为基础,本文提出协调活动的概念.
定义 13(协调活动). 给定部分正确协同业务过程 CBP=BP 1 ||BP 2 ||…||BP n ,CBP 对应的核 c=(C,c 0 ,C e ,A,Δ),称
a
活动 a∈A 1 ∪A 2 ∪…∪A n 为协调活动,当且仅当存在格局 c 1 ∈C,使得 c 1 ⎯⎯→ c 2 ,且 c 2 ∉C,其中,∀i∈[1..n],A i 为业务过
程 BP i 的活动集.
由定义 13 可知,协调活动是指在协同业务过程执行中若不加以控制,则可能导致隐藏路径产生的活动,即
从初始格局 c 0 至 c 2 或由 c 2 引出路径.因此,需要对这些活动进行协调,使其执行后到达正确格局 c 1 ,避免达到异
常格局 c 2 .而对于除协调活动以外的其他活动,由于其执行后总能够到达正确状态,因此无需协调.
以核为基础,映射生成修正业务过程之前需先将核中不相关活动(即不属于此业务过程及不是协调活动的
其他活动)隐藏,形式定义如下.
定义 14(隐藏). 给定部分正确协同业务过程 CBP,BP=(S,s 0 ,F,A,Δ)为 CBP 中一个业务过程,CBP 对应的核
c=(C,c 0 ,C e ,A,Δ),协调活动集为 A c ,则根据 BP 及 A c 对 c 进行隐藏后得到隐藏核为 c′=(C′,c′ 0 ,C′ e ,A′,Δ′),其中,
(1) C′=C;
(2) A′={τ}∪{a|∀(r,a,s)∈c.Δ∧a∈A∪A c };
(3) 对于∀(r,a,s)∈Δ,如果 a∈A∪A c ,则(r,a,s)∈Δ′,否则,τ格局迁移关系(r,τ,s)∈Δ′.
由定义 14 可知,隐藏是将 c 中格局迁移关系重置.即若格局迁移关系中活动是 BP 中活动或是协调活动,则
在重置的格局迁移关系中保持不变,否则将其设置为不可见活动τ.
在对 c 进行隐藏后,需要将产生的隐藏核 c′最小化以生成修正业务过程.当前,研究者提出多种行为最小化
技术 [19] ,如轨迹最小化、分支最小化及互模拟最小化等.由于本文关注协同业务过程间的路径一致,即路径对应
轨迹相同,因此我们采用文献[20]中提出的弱轨迹最小化算法对隐藏核进行最小化操作,最小化后生成一个中
间有穷自动机.本质上,标号迁移系统是一类特殊有穷自动机.因此,通过将中间有穷自动机中的状态集、开始状
态、结束状态集、活动集及状态迁移关系分别对应到标号迁移系统中的状态集、初始状态、终止状态集、活
动集及状态迁移关系,则可由隐藏核生成一个中间业务过程.这种转换过程非常直观,限于篇幅,这里不再赘述.
通过利用文献[20]中提出的最小化方法,可确保中间业务过程与隐藏核保持弱轨迹等价,且中间业务过程中不
含有不可见活动.
基于最小化后生成的中间业务过程,根据协调活动集,下面给出协调映射定义,以生成修正业务过程.