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

3152 Journal of Software 软件学报 Vol.31, No.10, October 2020

3 正确性分析

为了对协同业务过程进行修正,首先需要明确协同业务过程的正确性.目前,研究者提出多种针对协同业务
[9]
过程的正确性标准,其中,以合理性 及其变体(如弱合理 [11] 等)应用最为广泛.由于合理性主要用于定义组织内
业务过程的正确性且较为严格 [11] ,因此本文利用弱合理性定义协同业务过程的正确性.
定义 9(弱合理). 给定协同业务过程 CBP,c 0 和 c e 分别为初始格局和终止格局,称 CBP 是弱合理的,当且仅
σ
当对于从 c 0 可达的任意格局 c,存在迹σ,使得 c ⎯⎯→ c e .
从定义 9 可以看出,弱合理性要求从初始格局可达的任意格局都能够到达终止格局.这可确保每个业务过
程均能到达终止状态,因此可避免协同业务过程运行中可能出现的死锁和活锁等情形.同时,终止格局(见定义
3)要求每个业务过程的消息队列均为空,能够确保协同中产生的消息均可合理地被接收.
本文中的正确性分析是基于路径开展的.实际中的协同业务过程通常含有循环结构,循环结构将导致路径
数量和长度变为无穷,进而导致正确性检测无法判定.为了将问题收缩至有穷范围,同时记录下必要的循环结
构,本文定义简单路径如下.
n a
1 a
定义 10(简单路径). 设σ=c 0 ⎯⎯→ c 1 …c n−1 ⎯⎯→ c n …为协同业务过程 CBP 中的一条路径,称σ是简单路径,
当且仅当对于任意格局 c i 在σ中最多出现 2 次,即对于∀c i ,N={c j |c i =c j ∧j≠i}∧|N|≤2.
特别地,简单路径对应的轨迹称为简单轨迹.下面给出算法 1 用来计算一个协同业务过程中的简单路径.
Algorithm1. Generating simple routes.
Input: Collaborative business process CBP;
Output: Simple routes R;
1. curRoute=[c 0 ]; //a stack storing simple routes
2. visRoutes=[]; //a queue recording visited configurations
3. do
4. r=curRoute[len−1], and get all successors Su of r;
5. if Su=∅ then
6. save curRoute to R and add r into visRoutes;
7. curRoute=curRoute[0..len−3]; //backtrack node
8. else
//for a successor in Su, it can perform iff it occurs less than 2 times in curRoute or is in visRoutes
9. if all successor in Su cannot be executed then
10. save curRoute to R and add r into visRoutes;
11. curRoute=curRoute[0..len−3]; //backtrack node
12. else
a
13. get the transition r ⎯⎯→ s;
14. curRoute=curRoute∧a∧s;
15. end if
16. end if
17. while curRoute=∅
18. return R;
本质上,算法 1 是一种深度优先搜索算法.设 CBP 中格局数为 n,且在搜索过程中每个格局入栈次数为
⎛
⎞
{c 1 ,…,c n },则算法 1 的时间复杂度为 On× ∑ c .进一步地,对于∀i∈[1..n],根据定义 10 可知,c i 最大值为 2(对应
i ⎟
⎜
⎝ im ⎠ =
2
算法第 8 行),即 c i 存在于循环结构中被记录 2 次.因此,算法 1 在最坏情况下的时间复杂度为 O(2n ).特别地,由
于本文关注具有有穷状态空间的协同业务过程,即其中含有的格局数是有穷的.因此,可推出算法 1 是可以终止