对业务流程间的交互进行定义和分析, 是实现自上而下式跨组织业务流程建模需要解决的两个关键问题.

一方面, 为了实现不同组织业务流程间的有效协同, 有必要提供全局性的契约, 以规范业务流程间的交互.这种全局性的契约, 被学术界和工业界称为编排(choreography)^[1].为了定义编排, 大量编排建模语言被提出来, 例如BPMN 2.0^[2]、协作图(collaboration diagram, 简称CD)^[3]、Web服务编排规约语言(Web services choreography description language, 简称WS-CDL)^[4]、Let’s Dance^[5]、交互式Petri网IPN(interaction Petri nets, 简称IPN)^[6]、会话协议(conservation protocol, 简称CP)^[7]、BPEL4Chor^[8]、BPEL^gold[9]和消息序列图MSCs(message sequence charts)^[10].按照建模交互的方式, 这些编排建模语言可以分为互连式的编排建模语言和交互式的编排建模语言^[11].互连式的编排建模语言有交互式Petri网、BPEL4Chor和MSCs, 其特征是:将通信双方的通信活动进行对偶互连, 并用链接来表示业务流程间的消息交互^[12].交互式的编排建模语言有协作图、BPMN 2.0、WS-CDL、Let’s Dance、会话协议和BPEL^gold, 其特征是:将通信双方的通信活动视为原子交互, 并通过原子交互及原子交互间的依赖关系来描述多个业务流程间的消息交互^[12].与互连式的编排建模语言相比, 交互式的编排建模语言可以避免互连式编排建模语言存在的相容性问题

另一方面, 给定一个上述编排建模语言定义的编排, 参与者(peer)未必总能正确实现编排^[13].进一步来说, 给定一个编排, 从该编排映射得到每个参与者, 但这些参与者间的交互未必总能满足该编排.这就是可实现性(realizability)分析的内涵^[14].为了分析编排, 现有文献^{[1, 3, 7, 14-20]}主要以自动机或进程代数为形式化基础, 对编排进行可实现性分析.通常, 编排的可实现性分析包括3个步骤:(1)将编排映射为参与者; (2)将参与者经同步通信或异步通信组合为编排实现; (3)检验编排实现是否满足编排.其中, 第1步在很大程度上决定了可实现性分析的结果.

但是, 上述文献^{[1, 3, 7, 14-20]}在将编排映射为参与者时, 未考虑映射过程中不可见动作τ对行为的影响, 无法确保编排与参与者间的行为一致性.进一步地, 若编排与参与者间无法确保一致性, 则将影响编排可实现性分析的最终结果.

本文关注将编排映射为参与者, 其主要贡献如下.

(1)  提出了一种能够确保编排与参与者间行为一致的映射方法.该映射方法以Petri网作为形式化基础, 先通过动作映射, 将交互式Petri网定义的编排映射为带τ的交互式Petri网; 再提出τ删除规则, 对交互式Petri网中的τ进行有选择性的删除, 得到参与者; 最后, 从弱互模拟的角度, 证明本文所提出的τ删除规则的正确性, 即编排与参与者间满足行为等价, 保持了行为一致;

(2)  该映射方法已被实现成工具, 并通过实验表明本文所提出的映射方法的有效性.

本文第1节通过举例进一步分析拟解决的问题.第2节介绍相关基础.第3节讨论映射方法.第4节提出τ删除规则.第5节证明τ删除规则的正确性.第6节是工具与实验.第7节是相关工作的比较.最后对本文进行总结.

1 例子与问题分析

图 1是来自文献^[16]的例子.图 1(a)是使用会话协议描述的编排, 涉及3个角色:C(customer), V(vendor)和W(warehouse).会话协议的底层数学基础是自动机.在图 1(a)中, 圆圈代表状态, 有向边上的标号代表状态间的迁移动作, C→V:order表示Customer向Vendor发送了一个order.圆圈1表示开始状态, 同心圆圈6表示结束状态.图 1中(b)是参与者Customer, 从图 1(a)所示的编排通过动作映射而来.在图 1(b)中, 参与者具有3个不可见动作τ:状态2和状态3间的τ、状态3和状态4间的τ及状态3和状态5间的τ.图 1(c)是对图 1(b)使用τ移除操作(removal of tau transitions)^[14]得到的.与图 1(b)相比, 图 1(c)中没有τ.

现有文献^{[1, 3, 7, 14-20]}提出的映射方法通过两步, 将图 1(a)所示的编排映射为图 1(c)所示的参与者.

●  第1步, 根据角色(customer), 对图 1(a)所示的编排进行动作映射, 得到图 1(b)所示该角色对应的参与者, 即保留与该角色相关的动作, 把与该角色无关的动作映射为不可见动作τ.对图 1(a)而言, 图 1(b)与图 1(a)保持行为一致, 因为该步只将编排中与Customer无关的动作映射为τ.

●   第2步, 使用τ移除操作, 删除图 1(b)所示参与者中的3个不可见动作τ, 得到图 1(c)所示的参与者.对图 1(b)而言, 图 1(c)与图 1(b)行为不一致.究其原因在于, 图 1(b)所示的参与者中具有不确定性, 即从状态3出发存在两个相同的不可见动作τ; 而图 1(c)所示的参与者不存在不确定性.

综上分析可知, 图 1(a)所示的编排与图 1(c)所示的参与者间没有保持行为一致.事实上, 从弱互模拟的角度看(参见定义9), 图 1(b)所示的参与者和图 1(c)所示的参与者间并不满足弱互模拟.

造成编排与参与者间行为不一致的原因在于第2步, 即现有文献提出的映射方法均对参与者中的不可见动作τ全部删除, 未考虑τ对行为的影响.为此, 本文提出了一种能够确保编排与参与者间保持行为一致性的映射方法.该方法以Petri网作为形式化基础, 将图 1(a)所示的编排映射为图 1(d)所示的参与者.该参与者对应的可达图如图 1(e)所示.与图 1(b)相比, 图 1(e)所示的可达图删除了图 1(b)中状态2和状态3间的τ, 但保留了图 1(b)中状态3和状态4间的τ及状态3和状态5间的τ.也就是说, 本文所提出的映射方法对参与者中的τ进行有选择的删除, 而非全部删除.其目的是从弱互模拟的角度, 确保图 1(a)和图 1(e)之间满足行为等价, 即保证编排与参与者间的行为一致.

2 相关基础 2.1 Petri网

Petri网是1962年由德国科学家C. A. Petri博士在他的博士学位论文《用自动机通信》中创立的一种网状结构^[15], 它是一个有向二分图, 由库所和变迁组成, 其图形化的表示方式使得Petri网直观、易懂.通常, 库所使用圆圈表示, 变迁使用方框表示, 流关系使用有向线段表示, 托肯使用实心小黑点表示.

定义1(Petri网)^[21]. Petri网是一个四元组Σ=(P, T; F, M), 其中,

(1)    P∪T≠∅, 习惯称P为库所集, T为变迁集;

(2)    P∩T=∅;

(3)   F⊆(P×T)∪(T×P), 称F为流关系;

(4)   映射M:P→{0, 1, 2, 3, …}称为Petri网的一个标识, 通常用M₀表示Petri网的初始标识.

定义2(前集和后集)^[22]. 设Σ=(P, T; F, M)是一个Petri网, 若x∈P∪T, ^·x={y|(y, x)∈F∧y∈P∪T}, 则称^·x为x的前集; 若x∈P∪T, x^·={y|(x, y)∈F∧y∈P∪T}, 则称x^·为x的后集.

定义3(变迁发生规则)^[22].   设Σ=(P, T; F, M)是一个Petri网, 并具有以下变迁发生规则(transition firing rule).

1)   对于变迁t∈T, 如果∀p∈^·t:M(p)≥1, 则称变迁t在标识M有发生权(enable), 记为M[t〉.

2)   若M[t〉, 则在标识M下变迁t可以发生(fire), 从标识M发生变迁t得到一个新的标识M', 记为M'[t〉M, ∀p∈P, 满足:

    (1)  若p∈^·t-t^·, M'(p)=M(p)-1;

    (2)   若p∈t^·-^·t, M'(p)=M(p)+1;

    (3)  其他, M'(p)=M(p).

定义4(可达标识集)^[23]. 设Σ=(P, T; F, M₀)是一个Petri网, 其中, M₀是初始情态.Σ的可达标识集R(M₀)为满足下面条件的最小集合.

(1)   M₀∈R(M₀);

(2)   若M∈R(M₀), 且存在t∈T, 使得M'[t〉M, 则M∈R(M₀).

可达标识集R(M₀)描述了Σ所有可能的状态.满足条件(1)和条件(2)的可达标识集会有多个, 其中最小的一个只包含M₀及由M₀出发经过有限步变迁发生到达的那些标识, 即R(M₀).

若以R(M₀)中的元素为节点, 以有向弧描述标识间的后继关系, 就可以构造出Σ的可达图.

定义5(可达图)^[23].   设Σ=(P, T; F, M₀)是一个Petri网, 其中, M₀是初始情态.Σ的可达图定义为一个三元组RG(Σ)=(R(M₀), E, Tran), 其中,

(1)   E={(M_i, M_j)|M_i, M_j∈R(M₀), ∃t_k∈T:M_i[t_k〉M_j};

(2)   映射Tran:E→T称为迁移, Tran(M_i, M_j)=t_k当且仅当M_i[t_k〉M_j.

称R(M₀)为RG(Σ)的顶点集, E为RG(Σ)的弧集.若Tran(M_i, M_j)=t_k, 则称t_k为弧(M_i, M_j)的旁标, 通常将其记为

$ {{M}_{i}}\xrightarrow{{{t}_{k}}}{{M}_{j}}. $

2.2 编排和参与者

编排从全局视角描述了角色间的交互, 其关注点是角色间的消息交互.参与者从局部视角描述了该角色在编排中参与的交互, 其关注点是该角色在交互过程中的消息发送动作和消息接收动作.两者的区别在于:编排是角色间消息交互的全局契约; 参与者是该角色在编排中参与消息交互的的局部契约.

我们将经典的P/T网(参见定义1)扩展为交互式Petri网(参见定义6), 并使用交互式Petri网定义编排和参与者.具体而言, 使用交互式Petri网定义编排时, 变迁用于描述两个角色间的单次消息交互, 即某个角色向另一个角色发送了消息; 变迁点火序列用于描述角色间的消息发送序列.使用交互式Petri网定义参与者时, 变迁用于描述该角色在消息交互中的消息发送动作或消息接收动作; 变迁点火序列用于描述该角色在编排中的消息发送和消息接收序列.

定义6(交互式Petri网). 一个交互式Petri网是一个七元组IPN=(P, T, F, R, MT, M, λ), 其中,

(1)   P∪T≠∅∧P∩T=∅, 称P为库所集, T为变迁集;

(2)   F⊆(P×T)∪(T×P), 称F为流关系;

(3)   R为角色集合;

(4)   MT为消息集合;

(5)   映射M:P→{0, 1, 2, 3, …}称为Petri网的一个标识.通常用M₀表示Petri网的初始标识;

(6)   标记函数λ:T→L'∪L"∪{τ}, 用于给每个变迁指定字母表L’或L"中的一个标记或空标τ, 其中,

$ {L}'\left\{ {{r}_{1}}\_{{r}_{2}}\_m|{{r}_{1}}, {{r}_{2}}\in R\wedge m\in MT \right\}, {L}''=\left\{ xy|x\in \left\{ !, ? \right\}, y\in MT \right\}. $

引入3个辅助函数:发送者函数sf、接收者函数rf和消息mf.其中, sf:T→R, rf:T→R, mf:T→MT.

需要说明的是:

1)   与文献^[6]中定义的交互式Petri网(interaction Petri nets)相比, 定义6引入了标记函数λ, 用于建立变迁与标记间的映射, 其中, 标记存在3种形式:“角色A_角色B_消息”的格式、“?/!消息”或τ.“角色A_角色B_消息”表示角色A(发送者)向角色B(接收者)发送了消息, “?消息”表示消息发送动作, “!消息”表示消息接收动作.其中, “角色A_角色B_消息”用在编排定义中; “?/!消息”用在参与者定义中.

2)   当|R|＞1时, 交互式Petri网定义的是编排, 即使用交互Petri网描述多个角色间的消息交互; 当|R|=1时, 交互式Petri网定义的是单个角色对应的参与者, 即使用交互Petri网描述该角色对应的参与者在编排中的消息发送动作和消息接收动作.

3)   如果λ(t)≠τ, 则该变迁视为可见变迁; 否则, 视为不可见变迁.

4)   若变迁为可见变迁, 则该变迁对应的标记或为“角色A_角色B_消息”, 或为“?/!消息”.

图 2是使用交互式Petri网定义的编排, 该编排源于文献^[14]中使用协作图定义的火车站服务编排.该编排涉及4个角色:Customer(客户)、TrainStation(火车站)、Availability(车票检查组件)和Booking(车票预订组件), 其中, Customer是指火车票的预订者; TrainStation是指火车站的代理端, 用于接收用户的预订请求并返回预订结果; Availability用于检查是否有可用的火车票; Booking用于预订可用的火车票.图 2描述了下述交互场景.

●  首先, Customer向TrainStation发送请求消息(cus_ts_request);

●  其次, TrainStation与Availability间进行消息交互, 以检查火车票是否有可用的火车票(ts_ava_info, ava_ ts_infoAvail, ava_ts_itinerary);

●  然后, TrainStation与Booking间进行消息交互, 以预定可用的火车票(ts_boo_book, boo_ts_ack, boo_cus_ invoice);

●  最后, TrainStation把最终的结果发送给Customer(ts_cus_result).

其中, cus, ts, ava和boo分别是Customer, TrainStation, Availability和Booking的缩写.此外, 变迁null用于建模选择结构.

进一步地, 图 2所示的交互式Petri网指定了3个消息发送序列, 分别是:

(1)   cus_ts_request, ts_ava_info, ava_ts_infoAvail, ava_ts_itinerary^*, ts_boo_book, boo_ts__ack, ts_cus_result, boo_cus_invoice;

(2)   cus_ts_request, ts_ava_info, ava_ts_infoAvail, ava_ts_itinerary^*, ts_boo_book, boo_ts__ack, boo_cus_invoice, ts_cus_result;

(3)   cus_ts_request, ts_ava_info, ava_ts_infoAvail, ava_ts_itinerary^*, ts_boo_book, boo_ts__ack, ts_cus_result.

其中, *表示该消息发送发生0, …, n次.

图 3是由图 2所示的编排经本文所提出的映射方法得到的用使用交互式Petri网定义的4个参与者.需要注意的是, 图 3所示的Transtation和Availability中均有τ.这两个τ不能删除, 否则将造成编排与参与者间的行为不一致性.

2.3 弱互模拟

借鉴进程代数中的弱互模拟的定义^[23], 下面定义可达标识集上的弱互模拟.

定义7(实验关系)^[24].   设Σ=(P, T; F, M₀)是一个Petri网, 其中, M₀是初始情态.Σ的可达图为RG(Σ)=(R(M₀), E, Tran), M_i, M_j∈R(M₀), s∈Act^*, 其中, Act=T∪{τ}, 实验关系$\overset{\tau }{\mathop{\Rightarrow }}\, \text{和}\overset{s}{\mathop{\Rightarrow }}\, $定义如下.

(1)   ${{M}_{i}}\overset{\tau }{\mathop{\Rightarrow }}\, {{M}_{j}}$表示存在长度大于等于0的迁移序列${{M}_{i}}\xrightarrow{\tau }...\xrightarrow{\tau }{{M}_{j}}.$或更形式地, $\overset{\tau }{\mathop{\Rightarrow }}\, \overset{\text{def}}{\mathop{\text{=}}}\, {{\xrightarrow{\tau }}^{*}}, $其中, ${{\xrightarrow{\tau }}^{*}}\text{是}\xrightarrow{\tau }$的自反传递闭包.

(2)   令s=t₁…t_n, 则${{M}_{i}}\overset{s}{\mathop{\Rightarrow }}\, {{M}_{j}}$表示${{M}_{i}}\Rightarrow \xrightarrow{{{t}_{1}}}{{M}_{i+1}}...\Rightarrow \xrightarrow{{{t}_{n}}}{{M}_{i+n}}\Rightarrow {{M}_{j}}.$或更形式地, $\overset{s}{\mathop{\Rightarrow }}\, \overset{\text{def}}{\mathop{\text{=}}}\, \overset{\tau }{\mathop{\Rightarrow }}\, \xrightarrow{{{t}_{1}}}\overset{\tau }{\mathop{\Rightarrow }}\, ...$ $\xrightarrow{{{t}_{n}}}\overset{\tau }{\mathop{\Rightarrow }}\, $特别地, $\overset{t}{\mathop{\Rightarrow }}\, $表示在前面或者后面伴随着任意个$\xrightarrow{\tau }\text{的}\xrightarrow{t}$, 其中, t∈T.

定义8(弱模拟)^[24].   设Σ=(P, T; F, M₀)是一个Petri网, 其可达图为RG(Σ)=(R(M₀), E, Tran); Σ'=(P', T'; F', ${{{M}'}_{0}}$)是一个Petri网, 其可达图为RG(Σ')=(R(${{{M}'}_{0}}$), E', Tran’), 关系S是可达标识集R(M₀)∪R(${{{M}'}_{0}}$)的一个弱模拟, 当且仅当对于M₀S${{{M}'}_{0}}$, 下面的条件成立.

(1)   如果${{M}_{0}}\xrightarrow{\tau }{{M}_{k}}$其中, M₀, M_k∈R(M₀), 那么存在${{{M}'}_{k}}\in R({{{M}'}_{0}}),$满足${{{M}'}_{0}}\overset{\tau }{\mathop{\Rightarrow }}\, {{{M}'}_{k}}$且M_kS${{{M}'}_{k}};$

(2)   如果${{M}_{0}}\xrightarrow{t}{{M}_{k}}$, 其中, M₀, M_k∈R(M₀), 那么存在${{{M}'}_{k}}\in R({{{M}'}_{0}}), $满足${{{M}'}_{0}}\overset{t}{\mathop{\Rightarrow }}\, {{{M}'}_{k}}$且M_kS${{{M}'}_{k}}.$

如果M₀S${{{M}'}_{0}}$, 则称Σ被Σ'弱模拟.

定义9(弱互模拟)^[24]. 设Σ=(P, T; F, M₀)是一个Petri网, 其可达图为RG(Σ)=(R(M₀), E, Tran); Σ'=(P', T'; F', ${{{M}'}_{0}}$)是一个Petri网, 其可达图为RG(Σ')=(R(${{{M}'}_{0}}$), E', Tran’), 关系B是可达标识集R(M₀)∪R(${{{M}'}_{0}}$)上的弱互模拟当且仅当B和它的逆都是弱模拟.如果存在一个弱互模拟B满足M₀S${{{M}'}_{0}}$, 则称M₀和${{{M}'}_{0}}$是弱互模拟, 记作M₀≈${{{M}'}_{0}}$.

如果M₀B${{{M}'}_{0}}$, 则称Σ与Σ'间满足弱互模拟.

需要说明的是:进程代数中的弱模拟和弱互模拟是基于进程空间定义; 本文的定义8和定义9是基于可达标识集定义.

3 映射方法 3.1 方法概述

以图 2所示的编排为例, 本节介绍本文所提出的映射方法的基本思路, 如图 4所示.与现有文献^{[1, 3, 6, 7, 14-20]}所提出的映射方法相比, 本文所提出的映射方法将对参与者中的τ进行有选择的删除, 以确保编排与参与者间的行为一致性.具体而言, 该方法包含两个步骤:动作映射和τ删除.其中, 动作映射是指根据参与者的角色, 将交互式Petri网定义的编排映射为带τ的交互式Petri网; τ删除用于将带τ的交互式Petri网中的τ有选择地删除, 从而得到最终的参与者.

3.2 动作映射

动作映射的本质是根据角色, 将交互式Petri网定义的编排中与该角色相关的动作映射为消息发送动作或消息接收动作, 并把与该角色无关的动作映射为不可见动作τ, 具体可参见定义10的动作映射.

定义10(动作映射). 设IPN=(P, T, F, R, MT, M, λ)是一个交互式Petri网, 根据角色r∈R, 通过动作映射得到的交互式Petri网IPN'=(P', T', F', R', MT', M', λ'), 其中,

(1)   P'=P;

(2)    T'=T;

(3)    F'=F;

(4)    R'={r};

(5)    MT'={mf(t)|t∈T∧(sf(t)=r∨rf(t)=r};

(6)    M'=M;

(7)    λ'={(t, !mf(t))|t∈T∧λ(t)≠τ∧sf(t)=r}∪{(t, ?mf(t))|t∈T∧λ(t)≠τ∧rf(t)=r}∪{(t, t)|t∈T∧λ(t)=t}.

需要注意的是, 由于动作映射只是将编排中与该角色无关的动作映射为τ, 并不删除编排中的任何库所、变迁、托肯及弧, 所以我们认为, IPN'与IPN间保持了行为一致性.

根据角色TrainStation, 从图 2所示的编排中通过动作映射得到参与者, 如图 5所示.该交互式Petri网中具有1个τ, 由原编排中的变迁boo_cus_invoice映射而来.因为变迁boo_cus_invoice的发送者为Booking, 接收者为Customer, 均与角色TrainStation无关, 所以动作映射会将此变迁boo_cus_invoice映射为τ.

4 τ删除规则

针对第3.2节通过动作映射得到的带τ的交互式Petri网, 本节将提出τ的删除规则.对带τ的交互式Petri网中的τ进行删除时, 需要有选择地删除, 否则, 无法确保编排与参与者间的行为一致性.

4.1 τ删除规则1

τ删除规则 1. 设IPN=(P, T, F, R, MT, M, λ)是一个交互式Petri网, ∃t∈T∧λ(t)=τ, 若(^·t)^·={t}, 则该t可被删除, 得到新的交互式Petri网为IPN'=(P', T', F', R', MT', M', λ'), 其中,

(1)   P'=P-^· t;

(2)   T'=T-{t};

(3)   F'=F-{(x, t)|x∈^·t}-{(t, y)|y∈t^·}-{(x, y)|x∈^·(^·t)∧y∈(^·t)}∪{(x, y)|x∈^·(^·t)∧y∈t^·};

(4)   R'=R;

(5)    MT'=MT-{mf(t)};

(6)    λ'=λ-{(t, τ)};

(7)   若x∈^·t∧M(x)==0, 则M'=M; 若∀x∈^·t∧M(x)!=0, 则∀y∈t^·∧M'(y)=1.

τ删除规则1如图 6所示, 可应用在4种场景.粗箭头左边的是源交互式Petri网, 该交互式Petri网中有τ; 粗箭头右边的是目标交互式Petri网, 从源交互式Petri网中删除τ后得到.图 6(a)所示是将τ删除规则1应用于具有串行结构的交互式Petri网中.图 6(b)和图 6(c)所示是将τ删除规则1应用于具有并发结构的交互式Petri网中.图 6(a)和图 6(c)的区别在于对M'的处理不同.图 6(d)所示是将τ删除规则1应用于具有迭代结构的交互式Petri网中.

需要注意的是:为了直观区分τ和消息发送(接收)动作, 用带填充的黑色方块表示τ.此外, 虚线方块所示区域为删除τ的过程中, 源交互式Petri网中需要删除的相关元素.

4.2 τ删除规则2

τ删除规则 2. 设IPN=(P, T, F, R, MT, M, λ)是一个交互式Petri网, ∃t∈T∧λ(t)=τ, 若^·t=t^·, 则该t可被删除, 得到新的交互式Petri网为IPN'=(P', T', F', R', MT', M', λ'), 其中,

(1)   P'=P;

(2)   T'=T-{t};

(3)   F'=F-{(x, t)|x∈^·t}-{(t, y)|y∈t^·};

(4)   R'=R;

(5)   MT'=MT-{mf(t)};

(6)   λ'=λ-{(t, τ)};

(7)   M'=M.

τ删除规则2如图 7所示.图 7所示源交互式Petri网中的τ可以理解为单变迁的迭代, 执行次数为0, …, n. τ删除规则2用于将这个τ删除.

4.3 τ删除规则3

τ删除规则 3. 设IPN=(P, T, F, R, MT, M, λ)是一个交互式Petri网, ∃t₁, t₂, …, t_n∈T∧λ(t₁)=τ∧λ(t₂)=τ∧…∧λ(t_n)=τ, 若^·t₁=^·t₂…=^·t_n∧t₁^·=t₂^·=…=t_n^·, 则这n个t₁, t₂, …, t_n都可被删除, 得到新的交互式Petri网为IPN'=(P', T', F', R', MT', M', λ'), 其中,

(1)   P'=P-^·t₁;

(2)   T'=T-(^·t₁)^·;

(3)   F'=F-{(x, y)|x∈^·t₁∧y∈(^·t₁)^·}-{(x, y)|x∈(^·t₁)^·∧y∈t₁^·}-{(x, y)|x∈^·(^·t₁)∧y∈(^·t₁)}∪{(x, y)|x∈^·(^·t₁)∧y∈t₁^·};

(4)   R'=R;

(5)   MT'=MT-{mf(t₁)}-mf(t₂)}-...-{mf(t_n)};

(6)   λ'=λ-{(t₁, τ)}-{(t₂, τ)}-{(t_n, τ)};

(7)   若x∈^·t_i∧M(x)==0, 则M'=M; 若∀x∈^·t_i∧M(x)!=0, 则∀y∈t_i^·∧M'(y)=1.其中, i取值为1~n.

τ删除规则3可应用在两种场景下, 如图 8所示, 图 8(a)和图 8(b)的区别在于对M'的处理不同; 相同之处在于, 图 8(a)和图 8(b)所示的交互式Petri网中有n个τ, 且这些τ的输入汇聚于库所p₂, 输出汇聚于库所p₃.τ删除规则3用于将这些τ全部删除.

4.4 τ删除规则4

τ删除规则 4. IPN=(P, T, F, R, MT, M, λ)是一个交互式Petri网, ∃t₁, t₂, …, t_n, t∈T∧λ(t₁)=τ∧λ(t₂)=τ∧…∧λ(t_n)=τ∧ (t)≠τ, 若t₁=^·t₂=…=^·t_n=^·t∧t₁^·=t₂^·=…=t_n^·=t^·), 则(^·t₁)^·中的τ可以全部删除, τ变迁不能删除.同时, 必须增加1个τ以保持交互式Petri网中存在的选择时机, 得到新的交互式Petri网为IPN'=(P', T', F', R', MT', M', λ'), 其中,

(1) P'=P;

(2) T'=T-{x|x∈(^·t₁)^·∧λ(x)=t}∪{t_n+1};

(3) F'=F-{(x, y)|x∈^·t₁∧y∈(^·t₁)^·∧λ(y)=t}-{(x, y)|x∈(^·t₁)^·∧y∈t₁^·∧λ(x)=t}∪{(x, τ)|x∈^·t₁}∪{(τ, y)|y∈t₁^·};

(4) R'=R;

(5) MT'=MT-{mf(t₁)}-mf(t₂)}-...-{mf(t_n)};

(6) M'=M;

(7) λ'=λ.

τ删除规则4如图 9所示.图 9所示的源交互式Petri网中存在n个τ和1个消息发送动作!c, 且这些变迁的输入汇聚于库所p₂, 输出汇聚于库所p₃.若直接将这n个τ全部删除, 则会破坏源交互式Petri网中选择的时机, 从而使得删除前后两个Petri网间无法保持行为一致性.因而, 在把这n个τ删除以达到简化源交互式Petri网的同时, 还需在目标交互式Petri网中增加1个τ变迁, 用来保持源交互式Petri网中的选择时机.

5 τ删除规则的正确性分析

针对第4节提出的4个τ删除规则, 本节将对这4个规则的正确性进行分析.所谓正确性是指:源交互式Petri网与目标交互式Petri网间是否保持行为一致性.由于源交互式Petri网中存在不可见动作τ, 因而本文将采用弱互模拟作为检验行为是否一致的标准.这样, 我们就可以把检验源交互式Petri网与目标交互式Petri网间是否保持行为一致性的问题规约为检验源交互式Petri网与目标交互式Petri网间是否满足弱互模拟的问题.

基于上述分析, 下面给出行为一致性的定义.

定义12(行为一致). 设IPN=(P, T, F, R, MT, M, λ)是一个用交互式Petri网定义的编排, 源交互式Petri网IPN'= (P', T', F', R', MT', M', λ')是从IPN中通过动作映射得到的带τ的交互式Petri网, 目标交互式Petri网IPN"=(P", T", F", R", MT", M", λ")是对IPN'使用τ删除规则得到的交互式Petri网, 若IPN"和IPN'间满足弱互模拟, 则认为IPN和IPN"间保持行为一致.

5.1 τ删除规则1的正确性分析

对τ删除规则1进行正确性分析的关键问题是证明源交互式Petri网的可达图与目标交互式Petri网的可达图间是否满足弱互模拟.图 6所示的4组Petri网(如图 6(a)~图 6(d)所示)的可达图分别对应图 10所示的4组可达图(如图 10(a)~图 10(d)所示).在图 10所示的每组可达图中, 粗箭头左边对应的是源交互式Petri网的可达图, 粗箭头右边对应的是目标交互式Petri网的可达图填充圆圈表示该Petri网的结束标识.

下面证明图 10(a)所示的两个可达图间满足弱互模拟.

先证明图 10(a)中粗箭头左边的可达图被粗箭头右边的可达图所弱模拟.

●  第1步, 左边的可达图中, 有${{M}_{0}}\xrightarrow{\tau }{{M}_{1}};$右边的可达图中存在${{{M}'}_{0}}$, 使得${{{M}'}_{0}}\overset{\tau }{\mathop{\Rightarrow }}\, {{{M}'}_{0}}.$

●  第2步, 左边的可达图中, 有${{M}_{1}}\xrightarrow{!a}{{M}_{2}};$右边的可达图中存在${{{M}'}_{1}}$, 使得${M_1}\mathop \Rightarrow \limits^{!a} {M_2}.$

综上所述可知, M₀S${{{M}'}_{0}}$.关系$S=\{({{M}_{0}},{{{M}'}_{0}}),({{M}_{1}},{{{M}'}_{0}}),({{M}_{2}},{{{M}'}_{1}})\}.$

再证明关系S的逆${{S}^{-1}}=\{({{{M}'}_{0}}, {{M}_{0}}), ({{{M}'}_{0}}, {{M}_{1}}), ({{{M}'}_{1}}, {{M}_{2}})\}$是弱模拟, 即图 10(a)中粗箭头右边的可达图被粗箭头

左边的可达图所弱模拟.

●  第1步, 右边的可达图中, ${{{M}'}_{0}}$保持不变; 左边的可达图中存在M₀, 使得${{M}_{0}}\overset{\tau }{\mathop{\Rightarrow }}\, {{M}_{1}};$

●  第2步, 右边的可达图中, 有${{{M}'}_{0}}\xrightarrow{!a}{{{M}'}_{1}}$; 左边的可达图中存在M₂, 使得${{M}_{1}}\overset{!a}{\mathop{\Rightarrow }}\, {{M}_{2}}.$

综上所述, 可知${{{M}'}_{0}}$S^-1M₀.由此证明了M₀≈${{{M}'}_{0}}$.

同理, 我们也可证明图 10(b)~图 10(d)所示的两个可达图间满足弱互模拟.限于篇幅, 这里不一一证明.

5.2 τ删除规则2的正确性分析

图 7所示Petri网的可达图如图 11所示.

下面证明图 11所示的两个可达图间满足弱互模拟关系.

先证明图 11所示粗箭头左边的可达图被粗箭头右边的可达图所弱模拟.

●  第1步, 左边的可达图中, 有${{M}_{0}}\xrightarrow{!a}{{M}_{1}};$右边的可达图中存在${{{M}'}_{1}}$, 使得${{{M}'}_{0}}\overset{!a}{\mathop{\Rightarrow }}\, {{{M}'}_{1}};$

●  第2步, 左边的可达图中, 有${{M}_{1}}\xrightarrow{\tau }{{M}_{1}};$右边的可达图中存在${{{M}'}_{1}}$, 使得${{{M}'}_{1}}\overset{\tau }{\mathop{\Rightarrow }}\, {{{M}'}_{1}};$

●  第3步, 左边的可达图中, 有${{M}_{1}}\xrightarrow{?b}{{M}_{2}};$右边的可达图中存在${{{M}'}_{2}}$, 使得${{{M}'}_{1}}\overset{?b}{\mathop{\Rightarrow }}\, {{{M}'}_{2}};$

●  第4步, M₂和${{{M}'}_{2}}$均为结束标识.

综上所述, 可知M₀S${{{M}'}_{0}}$.关系$S=\{({{M}_{0}}, {{{M}'}_{0}}), ({{M}_{1}}, {{{M}'}_{1}}), ({{M}_{2}}, {{{M}'}_{2}})\}.$

再证明关系S的逆${{S}^{-1}}=\{({{{M}'}_{0}}, {{M}_{0}}), ({{{M}'}_{1}}, {{M}_{1}}), ({{{M}'}_{2}}, {{M}_{2}})\}$是弱模拟, 即图 11(a)中粗箭头右边的可达图被黑色箭

头左边的可达图所弱模拟.

●  第1步, 右边的可达图中, 有${{{M}'}_{0}}\xrightarrow{!a}{{{M}'}_{1}};$左边的可达图中存在M₁, 使得${{M}_{0}}\overset{!a}{\mathop{\Rightarrow }}\, {{M}_{1}};$

●  第2步, 右边的可达图中, 有${{M}_{1}}\overset{?b}{\mathop{\Rightarrow }}\, {{M}_{2}}.$左边的可达图中存在M₂, 使得${{M}_{1}}\overset{?b}{\mathop{\Rightarrow }}\, {{M}_{2}}.$

综上所述, 可知${{{M}'}_{0}}$S^-1M₀.由此证明了M₀≈${{{M}'}_{0}}.$

5.3 τ删除规则3的正确性分析

图 8所示两组Petri网的可达图分别对应图 12所示的两组可达图:图 12(a)和图 12(b).在图 12所示的每组可达图中, τ/τ/…/τ表示从n个τ变迁中选择一个变迁来发生.

(1) 证明图 12(a)所示的两个可达图间满足弱互模拟.

先证明图 12(a)中粗箭头左边的可达图被粗箭头右边的可达图所弱模拟.

●  第1步, 左边的可达图中, 有${{M}_{0}}\xrightarrow{!a}{{M}_{1}}$; 右边的可达图中存在${{{M}'}_{1}}$, 使得${{{M}'}_{0}}\overset{!a}{\mathop{\Rightarrow }}\, {{{M}'}_{1}};$

●  第2步, 左边的可达图中, 有${{M}_{1}}\xrightarrow{\tau }{{M}_{2}}$, 这里的τ可以是τ或者τ…或者τ; 右边的可达图中存在${{{M}'}_{1}}$, 使得${{{M}'}_{1}}\overset{\tau }{\mathop{\Rightarrow }}\, {{{M}'}_{1}};$

●  第3步, 左边的可达图中, 有${{M}_{2}}\xrightarrow{?b}{{M}_{3}}$; 右边的可达图中存在${{{M}'}_{2}}$, 使得${{{M}'}_{1}}\overset{?b}{\mathop{\Rightarrow }}\, {{{M}'}_{2}}.$

综上所述, 可知, M₀S${{{M}'}_{0}}$.关系$S=\{({{M}_{0}}, {{{M}'}_{0}}), ({{M}_{1}}, {{{M}'}_{1}}), ({{M}_{2}}, {{{M}'}_{1}}), ({{M}_{3}}, {{{M}'}_{2}})\}.$

再证明关系S的逆${{S}^{-1}}=\{({{{M}'}_{0}}, {{M}_{0}}), ({{{M}'}_{1}}, {{M}_{1}}), ({{{M}'}_{1}}, {{M}_{2}}), ({{{M}'}_{2}}, {{M}_{3}})\}$是弱模拟, 即图 12(a)中粗箭头右边的可达图被粗箭头左边的可达图所弱模拟.

●  第1步, 右边的可达图中, 有${{{M}'}_{0}}\xrightarrow{!a}{{{M}'}_{1}}$; 左边的可达图中存在M₁, 使得${{M}_{0}}\overset{!a}{\mathop{\Rightarrow }}\, {{M}_{1}};$

●  第2步, 右边的可达图中${{{M}'}_{1}}$保持不变; 左边的可达图中存在M₂, 使得${{M}_{1}}\overset{\tau }{\mathop{\Rightarrow }}\, {{M}_{2}};$

●  第3步, 右边的可达图中, 有${{{M}'}_{1}}\xrightarrow{?b}{{{M}'}_{2}}$; 左边的可达图中存在M₃, 使得${{M}_{2}}\overset{?b}{\mathop{\Rightarrow }}\, {{M}_{3}}.$

综上所述, 可知${{{M}'}_{0}}$S^-1M₀.由此证明了M₀≈${{{M}'}_{0}}.$

同理, 我们也可以证明图 12(b)所示的两个可达图间满足弱模拟关系.

5.4 τ删除规则4的正确性分析

图 9所示Petri网的可达图如图 13所示.

下面证明图 13所示的两个可达图间满足弱互模拟.

先证明图 13所示粗箭头左边的可达图被粗箭头右边的可达图所弱模拟.

●  第1步, 左边的可达图中, 有${{M}_{0}}\xrightarrow{!a}{{M}_{1}}$; 右边的可达图中存在${{{M}'}_{1}}$, 使得${{{M}'}_{0}}\overset{!a}{\mathop{\Rightarrow }}\, {{{M}'}_{1}};$

●  第2步, 左边的可达图中:或者有${{M}_{1}}\xrightarrow{\tau }{{M}_{2}}$, 右边的可达图中存在${{{M}'}_{2}}$, 使得${{{M}'}_{1}}\overset{\tau }{\mathop{\Rightarrow }}\, {{{M}'}_{2}}$; 或者有${{M}_{1}}\xrightarrow{!c}{{M}_{2}}$, 而右边的可达图中存在${{{M}'}_{2}}$, 使得${{{M}'}_{1}}\overset{!c}{\mathop{\Rightarrow }}\, {{{M}'}_{2}};$

●  第3步, 左边的可达图中, 有${{M}_{2}}\xrightarrow{?b}{{M}_{3}}$; 右边的可达图中存在${{{M}'}_{3}}$, 使得${{{M}'}_{2}}\overset{?b}{\mathop{\Rightarrow }}\, {{{M}'}_{3}};$

●  第4步, M₃和${{{M}'}_{3}}$均为结束标识.

综上所述, 可知, M₀S${{{M}'}_{0}}$.关系$S=\{({{M}_{0}}, {{{M}'}_{0}}), ({{M}_{1}}, {{{M}'}_{1}}), ({{M}_{2}}, {{{M}'}_{2}}), ({{M}_{3}}, {{{M}'}_{3}})\}.$

再证明关系S的逆${{S}^{-1}}=\{({{{M}'}_{0}}, {{M}_{0}}), ({{{M}'}_{1}}, {{M}_{1}}), ({{{M}'}_{2}}, {{M}_{2}}), ({{{M}'}_{3}}, {{M}_{3}})\}$是弱模拟, 即图 13(a)中粗箭头右边的可达

图被粗箭头左边的可达图所弱模拟.

●  第1步, 右边的可达图中, 有${{{M}'}_{0}}\xrightarrow{!a}{{{M}'}_{1}}$; 左边的可达图中存在M₁, 使得${{M}_{0}}\overset{!a}{\mathop{\Rightarrow }}\, {{M}_{1}}.$

●  第2步, 右边的可达图中:或者要么有${{{M}'}_{1}}\xrightarrow{\tau }{{{M}'}_{2}}$, 左边的可达图中存在M₂, 使得${{M}_{1}}\overset{\tau }{\mathop{\Rightarrow }}\, {{M}_{2}}$; 或者要么有${{{M}'}_{1}}\xrightarrow{!c}{{{M}'}_{2}}$, 左边的可达图中存在M₂, 使得${{M}_{1}}\overset{!c}{\mathop{\Rightarrow }}\, {{M}_{2}}.$

●  第3步, 右边的可达图中, 有${{{M}'}_{2}}\xrightarrow{?b}{{{M}'}_{3}}$; 左边的可达图中存在M₃, 使得${{M}_{2}}\overset{?b}{\mathop{\Rightarrow }}\, {{M}_{3}}.$

综上所述, 可知${{{M}'}_{0}}$S^-1M₀.由此证明了M₀≈${{{M}'}_{0}}.$

6 工具与实验 6.1 工具设计与实现

图 14是我们实现的工具Chor2Peer的结构.其中, PIPE v4.3.0是一个图形化的Petri网建模和分析工具^[25]; IPN表示使用交互式Petri网定义的编排; Projection是映射模块, 用以实现第3节提出的动作映射, 对交互式Petri网中的变迁进行映射, 得到带τ的交互式Petri网; TauDeletion是tau删除模块, 用以实现第4节提出的τ删除规则, 对带τ的交互式Petri网中的τ进行有选择性地删除，得到参与者.图 15是工具实现的界面截图.

6.2 对比实验

本文选取了5篇具有代表性的文献^[14-18], 将本文所提出的映射方法与这些文献中所提出的映射方法做对比, 具体实验结果见表 1、表 2.

表 1、表 2的第1列为序号, 其中, 序号1对应的是文献^[15], 序号2对应的是文献^[16], 序号3对应的是文献^[17], 序号4对应的是文献^[18], 序号5对应的是文献^[14].表 1第2列是该文献定义的编排; 第3列是该文献映射产生的参与者; 第4列是根据第2列所示编排, 使用交互式Petri网定义的编排.表 2第2列是使用本文所提出的映射方法产生的使用交互式Petri网定义的参与者; 表 2第3列是该参与者对应的可达图.需要说明的是, 在表 1的第1列中, 序号1~序号4所对应的参与者使用自动机定义, 有向箭头指向的圆圈表示开始状态, 同心圆圈表示结束状态; 序号5所对应的参与者使用标号迁移系统定义, 有向箭头指向的圆圈表示开始状态, 同心圆圈表示结束状态.通过对比表 1第3列和表 2第3列可知, 现有文献将编排映射为参与者时, 未考虑τ对行为的影响, 将其全部删除, 无法确保编排与参与者间的行为一致性.限于篇幅, 这里不一一证明编排与参与者间不满足弱互模拟.本文所提出的方法则考虑了τ对行为的影响, 有选择地删除τ, 可确保编排与参与者间满足弱模拟, 保持行为一致性.

表 1、表 2中使用本文所提出的映射方法得到的参与者, 表 3记录了使用Chor2Peer工具生成每个参与者对应的库所数量、变迁数量、τ变迁数量、弧关系数量及映射时间.值得注意的是:

(1) 映射时间主要由3部分组成:判断Petri网中的结构特征并选择删除规则、删除τ变迁重构Petri网及遍历Petri网.

(2) 参与者具有的库所、变迁、τ变迁及弧的数量越多, 这意味着编排到参与者映射过程中τ变迁删除操作越少, 因而映射时间就越短.

(3) 表 3中序号1对应的参与者P和R, 虽然P拥有的库所、变迁、τ变迁及弧的数量比R的多, 但P的映射过程中遍历Petri网2次, 而R只遍历Petri网1次, 因此P的映射时间比R的长.

(4) 表 3中序号3对应的参与者A和C, 虽然C拥有的库所、变迁、τ变迁及弧的数量比A的多, 但C的映射过程中判断Petri网结构特征并选择删除规则的时间比A多, 因此C的映射时间比A的长.

7 相关工作

按形式化基础, 现有文献^{[1, 3, 6, 7, 14-20]}主要以自动机或进程代数作为底层基础, 讨论编排到参与者的映射.

以自动机作为形式化基础方面, 文献^[7]针对自动机定义的会话协议, 最早提出了会话协议可实现需满足的3个充分条件:无损连接(lossless join)、同步兼容(synchronous compatible)、自治性(autonomous).文献^[15]讨论了不同类型的协作图, 即协作图(collaboration diagram)、协作图集(collaboration diagram set)和协作图图(collaboration diagram graph)的可实现性问题, 并说明了这3种协作图的可实现性问题均可规约为会话协议的可实现性问题.文献^[16]讨论了3种不同的可视化形式主义, 即协作图、消息序列图(message sequence charts)及会话协议建模交互的异同, 并详细论述了可实现性和同步性(synchronizability).文献^[3]针对协作图, 最早提出了协作图可实现需满足的充分条件:该协作图是分离的(seperated), 且每个事件是好通知的(well-informed).与会话协议相比, 协作图无法描述除单消息循环外的其他消息循环.文献^[1]研发了一个工具:(1)用于检测协作图定义的交互的可实现性; (2)用于验证协作图定义的交互的LTL性质; (3)用于从协作图中合成参与者(peer).文献^[17]针对一类任意发起人的会话协议(arbitrary-initiator protocol), 即存在一个状态多个参与者可以发送消息, 由于文献^[7]提出的充分条件用于分析该类会话协议的可实现性时会产生假阳性(false positive), 提出了一种新颖的算法, 用于判断该类会话协议的可实现性.文献^[17]针对在异步通信模型下会话协议的可实现性不可判定的不足, 通过同步性性质(synchronizability property), 提出了一个充分必要条件, 用于检验会话协议的可实现性.文献^[18]针对不可实现的会话协议, 提出了一种方法, 通过监视器(monitor)和迭代增加的同步消息来强迫系统满足会话协议, 从而使得该会话协议成为可实现的.但是, 文献^{[1, 3, 7, 16-19]}将协作图或会话协议定义的编排映射为基于有限状态机定义的参与者时, 均使用ε-move操作将映射产生的τ全部删除, 未考虑τ对行为的影响, 无法确保编排与参与者间的行为一致性.

在以进程代数作为形式化基础方面, 文献^[18]针对BPMN 2.0编排(BPMN 2.0 choreographies), 提出了一种检测BPMN 2.0编排可实现性的方法.该方法将BPMN 2.0编排编码为使用LOTOS NT定义的进程表达式, 并在工具的支持下, 使用等价性检测技术实现了对BPMN 2.0编排可实现性的自动检测.文献^[14]针对协作图提出了一种检测协作图可实现性的方法.该方法将协作图编排编码为使用LOTOS NT定义的进程表达式, 并在工具的支持下, 使用等价性检测技术实现了对协作图可实现性的自动检测.但是, 文献^{[14, 20]}在将BPMN 2.0或协作图定义的编排映射为基于标号迁移系统定义的参与者时, 也使用“ε-move”操作将映射产生的τ全部删除, 未考虑τ对行为的影响, 无法确保编排与参与者间的行为一致性.

在现有文献中, 只有文献^[6]以Petri网作为形式化基础, 讨论编排到参与者的映射.文献^[6]将Petri网扩展为交互Petri网, 用于建模编排, 并提出了映射方法, 将交互式Petri网定义的编排映射为交互式Petri网定义的参与者.但是该文献也未考虑τ对行为的影响, 无法确保编排与参与者间的行为一致性.以图 1(a)所示的编排为例, 使用文献^[6]所提出的映射方法得到的参与者Customer也如图 1(c)所示.该映射方法将使用文献^[6]提出的两种约简规则(reduction rules)把映射产生的τ全部删除.

8 结束语

本文以Petri网作为形式化基础, 提出了一种能够确保编排与参与者间行为一致的映射方法.首先, 该方法通过动作映射, 将交互式Petri网定义的编排映射为带τ的交互式Petri网; 其次, 提出了4条τ删除规则, 用于有选择地删除带τ的交互式Petri网中的τ, 得到参与者; 然后, 从弱互模拟的角度证明了上述4条τ删除规则的正确性, 即可确保编排与参与者间的行为一致性; 最后, 通过实验验证了该方法的有效性.

本文的不足在于:4条tua删除规则基于交互式Petri网的结构特征定义.若一个交互式Petri网具有可以删除的τ, 但不满足上述4条规则对应的结构特征, 那么本文所提出的映射方法将无法将其删除.因此, 下一步的工作重点是提出交互式Petri网的化简规则, 并证明这些化简规则针对这些结构特征而言是完备的.