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

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

际场景来定义.本文同时考虑活动间同步交互及基于消息通信的活动间异步交互,参见定义 5.
对于任意协同业务过程,其状态用格局来表示.它由每个参与组织的运行状态及所配置的先进先出消息队
列组成向量表示,其形式定义如下.

定义 3(格局). 协同业务过程 CBP 状态表示为一个格局 c=〈s 1 ,Q 1 ,…,s n ,Q n 〉,其中,∀i∈[1..n],s i 为业务过程 BP i
的运行状态;Q i 为业务过程 BP i 的先进先出消息队列,用来存储其接收消息,本文中 Q i 的长度默认为无穷.
特别地,CBP 的初始格局记为 c 0 =〈s 01 ,NIL,…,s 0n ,NIL〉,其中,∀i∈[1..n],s 0i 为 BP i 的初始状态,且其消息队列为
空,即为 NIL;CBP 的终止格局记为 c e =〈s e1 ,NIL,…,s en ,NIL〉,其中,∀i∈[1..n],s ei 为 BP i 的终止状态,且其消息队列为
空,表示所有的消息均被接收.
可对格局中的运行状态及消息队列进行重置,形式定义如下.
/ ′
定义 4(格局重置). 设格局 c=〈s 1 ,Q 1 ,…,s n ,Q n 〉,将业务过程 BP i 的运行状态由 s i 重置为 s′ i ,记为 c[ s s ],而将
i i
/ ′
BP i 的消息队列由 Q i 重置为 Q′ i ,记为 c[ QQ ].
i i
在协同业务过程中,活动执行除了受到本地控制流的约束外,还受到其他业务过程中活动执行情况的影响.
归纳起来,可分为如下 3 种情况.
1) 若 a∈A l ,则活动 a 执行仅受到本地控制流的影响;
2) 若 a∈A si ,则活动 a 执行除了受到本地控制流的影响外,还需要所有含有同步交互活动 a 的业务过程同时
参与完成;
3) 若 a=!m,则活动 a 执行除了受到本地控制流的影响外,还受到其他需要接收消息 m 的业务过程的消息
队列 Q 的影响,即 Q 不满,且存在接收消息 m 的业务过程 BP.在发送消息 m 之后,消息 m 被添加至 BP 消息队列
的尾部;而若 a=?m,则活动 a 执行除了受到本地控制流的影响外,还受到自身消息队列 Q 的影响,即 Q 不空,且 Q
的第 1 个元素是消息 m.在接收消息 m 之后,消息 m 从 Q 的头部移除.
根据上述对活动执行情况的分析,我们定义协同业务过程点火规则.
定义 5(点火规则). 设 CBP=BP 1 ||BP 2 ||…||BP n 为一个协同业务过程,其格局为 c=〈s 1 ,Q 1 ,…,s n ,Q n 〉,则其点火规
则定义如下.
a
a
/ ′
(1) 若 a∈A l ,则 c ⎯⎯→ c′,当且仅当 s i ⎯⎯→ s′ i ∧c′=c[ s s ];
i i
/ ′
a
a
(2) 若 a∈A si ,则 c ⎯⎯→ c′,当且仅当∀a∈ A (1≤j≤n):s j ⎯⎯→ s′ j ∧c′=c[ s s ];
j
j
si
j
a a ! ?
i j
(3) 若 a=!m,则 c ⎯⎯→ c′,当且仅当 s i ⎯⎯→ s′ i ∧∃i,j∈[1..n]:m∈ M ∩ M ∧|Q j |<L Q j (L Q j 是 Q j 的长度 )
/ ′
/ ′
∧Q′ j =Q j m∧c′=c[ QQ ]∧c′=c[ s s ];
j j i i
a
/ ′
/ ′′
a
(4) 若 a=?m,则 c ⎯⎯→ c′,当且仅当 s i ⎯⎯→ s′ i ∧Q i =mQ″ i ∧c′=c[ QQ ]∧c′=c[ s s ].
i i i i
特别需要说明的是,给定协同业务过程 CBP,若利用点火规则可产生无穷个格局,则称 CBP 具有无穷状态空
间,否则称其具有有穷状态空间.本文关注具有有穷状态空间的协同业务过程.
基于点火规则,我们可定义协同业务过程的行为,表示为路径.下面给出几个与路径相关的定义.
定义 6(路径). 给定协同业务过程 CBP,其行为表示为路径,是 CBP 的格局和活动(即本地活动或交互活动)
n a
i a
1 a
组成的有穷或无穷序列.对于任意路径σ,其形如:c 0 ⎯⎯→ c 1 …c n−1 ⎯⎯→ c n …,其中,∀i∈[1..n],迁移 c i−1 ⎯⎯→ c i 符
合定义 5 给出的点火规则,c i 为 CBP 的格局,c 0 为初始格局.
1 a
n a
定义 7(路径的轨迹). 对于任意路径 r,r=c 0 ⎯⎯→ c 1 …c n−1 ⎯⎯→ c n …,则将 r 中的活动依次连接,得到活动执
行序列 l=a 0 ∧a 1 …a n−1 ∧a n ∧…称为 r 的迹,表示为 trace(r).
l
特别地,若格局 c 可通过执行迹 l 迁移至格局 c′,则记为 c ⎯⎯→ c′.
n b
1 a
n a
1 b
定义 8(路径一致). 设 r p =c p0 ⎯⎯→ c p1 …c p(n−1) ⎯⎯→ c pn 和 r q =c q0 ⎯⎯→ c q1 …c q(n−1) ⎯⎯→ c qn 为两条有穷路
径,称 r p 和 r q 一致,记为 r p =r q ,当且仅当 r p 的迹与 r q 的迹相同.