基于Petri网分析编排的可实现性

黄 苾,代 飞+,王亚博,莫 启,曹 涌,王雷光

(1.西南林业大学 大数据与智能工程学院,云南 昆明 650224;2.云南大学 软件学院,云南 昆明 650091)

1 问题的描述

服务计算技术的快速发展使软件系统呈现出越来越多的分布式并发特性，系统的不同服务参与者之间需要遵守相应的规约进行协同交互。并发分布式系统中常用的交互机制是基于消息的通信。为有效地将这些分布在不同组织、独立开发的参与者进行集成，有必要提供参与者参与协同应遵守的规约，通常称为编排(choreography)，用于从全局视角，指定参与者间的交互。目前，已有许多编排规约语言，如：BPMN 2.0[1]编排、Let’s Dance[2]、协作图(Collaboration Diagram, CD)[3]、Web服务编排规约语言(Web Services Choreography Specification Language, WS-CDL)[4]、交互式Petri网(Interaction Petri Nets, IPN)[5]、会话协议(Conservation Protocol, CP)[6-7]、进程代数LOTOS[8]，被提出用于建模编排。

在编排分析中，一个重要的问题是可实现性，即编排规约是否可由一组通过消息传递进行通信的参与者实现[9]。更准确地说，编排的可实现性分析可以准确描述为：

(1)

式中：C表示编排，Peeri表示由编排产生的参与者i，‖表示在不同通信模型下参与者间的并发组合，=表示在不同语义下的等价检测，?表示等号两边未必满足等价检测。

根据使用的形式化方法，现有编排可实现性分析方法大致可以分为使用自动机的分析方法、使用进程代数的分析方法和使用Petri网的分析方法3类。在使用自动机的分析方法中，针对会话协议定义的编排，文献[10]以自动机作为形式化基础，提出了检测会话协议可实现需要满足的3个充分条件：无损连接(lossless join)、同步兼容(synchronous compatible)、自治性(autonomous)。在此基础上，文献[11]针对会话协议的子类，提出了同步性条件(synchronizability conditions)，用于检测会话协议的可实现性。文献[12]对任意发起者的会话协议(arbitrary-initiator protocols)进行了可实现性分析。文献[9]提出了会话协议可实现的充分必要条件，使用现有的行为等价检测工具和模型检测工具，对会话协议的可实现性进行了自动检测。在使用进程代数的分析方法中，文献[8]以进程代数LOTOS NT作为形式化基础，提出一种把协作图转换为LOTOS NT进程表达式的方法，从强互模拟的角度，分析了协作图的可实现性。针对BPMN 2.0编排，文献[13]以进程代数LOTOS NT作为形式化基础，提出一种把BPMN 2.0编排转换为LOTOS NT进程表达式的方法，从强互模拟的角度，分析了BPMN 2.0编排的可实现性。在使用Petri网的分析方法中，文献[5]以Petri网作为形式化基础，分析了同步通信下编排的可实现性。

与上述工作相比，本文工作的最大不同在于：使用Petri网实现了对同步通信和有界异步通信下编排的可实现性分析。其主要贡献如下：

(1)给定一个编排，提出了编排到参与者的生成算法；

(2)在同步通信下，分析了编排的可实现性；

(3)在有界异步通信下，分析了编排的的可实现性。

如图1所示概述了本文方法，分为4步：第一步参与者的映射生成，具体参见第3章;第二步同步并发组合和异步并发组合，分别参见4.1节和4.3节;第三步在Petri网的开源工具(Platform Independent Petri net Editor 2, PIPE)[14]支持下可自动实现，PIPE是一个开源的图形化的Petri网建模和分析工具;第四步行为等价检测，具体参见4.2节和4.3节。

2 Petri网和交互式Petri网

2.1 Petri网

定义1Petri网。Petri网是一个三元组N=(P,T;F)，其中：

(1)P∪T≠∅，P是库所的集合，T是变迁的集合；

(2)P∩T=∅；

(3)F⊆(P×T)∪(T×P)是弧的集合(流关系)。

通常，在Petri网的图形化表示中，库所用圆圈表示，变迁用矩形方框表示。

令X=P∪T，对于节点x∈X,·x={y|(y,x)∈F∧y∈P∪T}称为x的前集；对于x∈X,x·={y|(x,y)∈F∧y∈P∪T}称为x的后集。

定义2Petri网的语义。令N=(P,T;F)是一个Petri网，有：

(1)M:P→是N的一个状态，也称为标识(Marking)，表示库所中托肯的分布。其中是非负整数的集合。M(p)表示库所p中的托肯数，托肯通常用小黑点表示；

(2)变迁t∈T在状态M是使能的(enabled)，当且仅当每个输入库所都包含至少一个标记，即∀p∈·t：M(p)≥1；

(3)一个使能的变迁t发生点火，则t从p∈·t中消耗一个托肯，在p∈t·中产生一个托肯；

通常，使用(N,M0)表示一个拥有初始状态M0的Petri网。

定义3可达标识集。设(N,M0)是一个拥有初始状态M0的Petri网，可达标识集R(M0)为满足下面条件的最小集合：

(1)M0∈R(M0)；

(2)若M∈R(M0)，且存在t∈T，使得M[t>M′，则M′∈R(M0)。

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

定义4可达图。设(N,M0)是一个拥有初始状态M0的Petri网，可达图定义为一个三元组RG(N)=(R(M0),E,Tran)，其中：

(1)R(M0)为顶点集；

(2)E={(Mi,Mj)|Mi,Mj∈R(M0),tk∈T:Mi[tk>Mj}为弧集；

定义5隐式库所。设(N,M0)是一个拥有初始状态M0的Petri网，库所p∈P是隐式库所(implicit place)，当且仅当：∀t∈p·,∀M∈R(M0):M≥·t-{p}M≥·t。

删除隐式库所并不改变Petri网的行为，更多知识请参见文献[15]。

2.2 交互Petri网

本文使用文献[16]中提出的交互式Petri网作为形式化基础，并使用交互式Petri网建模编排。

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

(1)N=(P,T;F)是Petri网；

(2)M表示N的状态；

(3)R为角色集合；

(4)MT为消息集合；

(5)标记函数λ:T→L′∪L″∪MT∪{τ},用于给每个变迁指定集合L′或L″或MT或{τ}的一个标记，其中：L′={r1_r2_m|r1,r2∈R∧m∈MT},L″={xy|x∈{!,?},y∈MT}。

需要注意的是：

(1)定义6引入了标记函数λ，用于建立变迁与标记间的映射。其中，标记存在4种形式：“参与者A_参与者B_消息”、“?/!消息”、“消息”和“τ”。其中：“参与者A_参与者B_消息”表示参与者A与参与者B间的双向交互(two-way interaction)，即参与者A先向参与者B发送了初始消息后，参与者B再向参与者A发送返回消息;“?消息”表示消息发送动作，“!消息”表示消息接收动作;“消息”表示参与者间交互的消息；τ表示不可见变迁。

(2)当|R|>1时，交互式Petri网定义的是编排或编排实现，两者的区别在于：编排中变迁的标记格式为“参与者A_参与者B_消息”，而编排实现中变迁的标记格式为“?/!消息”或“消息”；当|R|=1时，交互式Petri网定义的是参与者。

(3)若λ(t)==τ，则该变迁为不可见动作；若λ(t)≠τ，该变迁为可见动作。

图2是使用交互式Petri网定义的编排，该案例源于文献[13]中的订票系统。该编排涉及4个参与者：客户端client(简写cl)、订票系统booking system(简写bs)、银行服务bank service(简写bk)和数据库database(简写db)，描述了下述交互场景：

(1)客户端向订票系统发送建立链接消息(connect)；接着向订票系统发送请求消息(request1)，然后，订票消息向客户端发送响应消息(reply)。

(2)客户端或向订票系统发送退出消息(quit)，或向订票系统发送另外一个请求消息(request2)，或向订票系统发送一个预订请求消息(book)。

对于上述最后一种情况，客户端向银行服务发送付款消息(pay)，然后，订票系统向数据库发送存储本次事务的消息(store)。

如图2所示，编排是不可实现的。更准确地说，在同步通信下，该编排是不可实现的；在异步通信下，该编排也是不可实现的。因为在图2所示的编排中，订票系统描述了这样的消息序列：cl_bs_connect,bl_bs_request1,bs_cl_reply,cl_bs_book,cl_bk_pay,bs_db_store。但是，在同步通信和异步通信下，由参与者并发组合构成的编排实现中存在这样的消息序列：cl_bs_connect,bl_bs_request1,bs_cl_reply,cl_bs_book,bs_db_store,cl_bk_pay。在该消息序列中，消息bs_db_store和cl_bk_pay交换了位置。

3 参与者生成

可实现性分析首要解决的问题是如何从编排中生成参与者。参与者从局部视角描述了该角色在协同中参与的交互。编排到参与者生成的基本思路为：根据角色，通过映射操作，将编排中与该角色相关的变迁的标记格式从“参与者A_参与者B_消息”映射为“?消息”或“!消息”，将编排中与该角色无关的变迁格式从“参与者A_参与者B_消息”映射为τ；再使用约简(reduction)操作，从映射得到的交互式Petri网中删除τ变迁。

定义7映射。设IPN=(P,T;F,R,MT,M,λ)是一个交互式Petri网，指定角色r∈R，映射得到的交互式Petri网IPN′=(P′,T′,F′,R′,MT′,M′,λ′)，其中：P′=P;T′=T;F′=F;R′={r};MT′={MC(t)|t∈T∧(SP(t)=r∨RP(t)=r};M′=M;

λ′={(t,!MC(t))|t∈T∧λ(t)τ∧SP(t)=r}∪{(t,?MC(t))|t∈T∧λ(t)τ∧RP(t)=r}∪{(t,τ)|t∈T∧λ(t)=τ}，SP={r1|t∈T∧λ′(t)=r1_r2_m∈L′}表示变迁对应的消息发送者，RP={r2|t∈T∧λ′(t)=r1_r2_m∈L′}表示变迁对应的消息接收者，MC={m|t∈T∧λ′(t)=r1_r2_m∈L′}表示变迁对应的消息。

需要注意的是：映射并不删除交互式Petri网中的任何库所、变迁、托肯及弧。

约简操作见算法1，该算法分为两个阶段：第一阶段(代码第4～6行)，用于增加新的库所和流关系，并连接变迁τ的前驱变迁和后继变迁；第二阶段(代码第7～9行)，用于删除与变迁τ相关的流关系、库所和变迁τ本身。令m和n分别表示交互式Petri网中变迁的数量和库所的数量。算法1的最坏时间复杂度为O(m×n2)。

算法1Reduction Operation。

输入:IPN=(P,T;F,R,MT,M0,λ)是一个带τ的交互式Petri网；

输出:IPN=(P,T;F,R,MT,M0,λ)。

1 foreach t∈T do

2 if λ(t)==τ then

3 foreach(p1,p2)∈·t×t·do

4 P=P∪{p12} //p12是新增的库所

5 M0(p12)=M0(p1)+M0(p2)

7 F=F-{(p,t)|(p∈·t)}∪{(t,p)|(p∈t·)}//删除流关系

8 P=P-(·t∪t·)//删除库所

9 T=T-{t}//删除变迁

10 return(P,T;F,R,MT,M0,λ)

图3直观地展示了约简操作。箭头左边所示的Petri网带有τ，虚线有向线段、虚线方框和虚线圆圈表示约简操作中将要删除的流关系、变迁和库所；箭头右边所示的Petri网是经约简操作后得到，虚线有向线段、虚线方框和虚线圆圈表示约简操作中将要新增的流关系、变迁和库所。

对于图2所示的订票系统，通过动作映射和约简操作，映射生成的参与者客户端、订票系统、银行服务和数据库，如图4所示。

4 可实现性

本文考虑映射可实现性。映射可实现性是指，如果编排指定的交互，与由编排映射生成的参与者间的交互一样，则编排是可实现的。这是多数文献[6-9]中使用的可实现性定义。

本文使用行为等价检测，提出通过比较编排可达图与编排实现可达图，来实现对编排的可实现性分析。如果两个可达图是行为等价的，则认为参与者准确实现了编排，编排是可实现的；若两个可达图不满足行为等价，则认为编排是不可实现的。进一步，行为等价检测可通过检测两个可达图是否满足强互模拟关系[17]和弱互模拟关系[18]来实现。

下面给出映射可实现性的定义。

定义8映射可实现性。一个由交互式Petri网定义的编排C=(P,T;F,R,MT,M,λ)是可实现的，当且仅当，RG(C)与RG(CP)是行为等价的，其中：CP=(Peer1‖Peer2‖…‖Peern)为由参与者通过并发组合构建的编排实现，Peeri表示由编排C映射生成的参与者i；‖表示并发组合。

在同步通信和异步通信下，‖并发组合具有不同的语义，具体可参见4.1节和4.3节。

4.1 同步并发组合

本质上，同步通信是一种阻塞模式，它是指当发送者发出初始消息后，需等待接收者发回响应消息后，才能发送下一个消息的通信方式。

图5给出了使用交互式Petri网实现同步通信的思路(在图5a中，PeerA与PeerB间关于消息m1和消息m2存在同步通信，由虚线无向线段相连)，通过两步完成：

(1)通过使用基于消息互补的变迁熔合技术，将图5a简化为图5b。消息互补是指：两个变迁对应的标号中消息名相同，但前缀不同。例如，在图5a中，PeerA中的变迁“!m1”和PeerB中的变迁“?m1”是消息互补的。变迁合成是把两个消息互补的变迁合成为一个变迁。例如，在图5a中，可以将PeerA中的变迁“!m1”和PeerB中的变迁“?m1”合成为图5b中的变迁“m1”。

(2)通过使用删除隐式库所的技术，将图5b简化为图5c。不难发现，在图5b中虚线圆圈所示的库所都是隐式库所，可以删除。

同步并发组合是指在同步通信环境下，将多个参与者并发组合为编排实现。下面给出同步并发组合的定义。

定义9同步并发组合。设Peeri=(Pi,Ti;Fi,Ri,MTi,Mi,λi)(i=1,2)是两个参与者，其中，存在m∈MT1∩MT2，t1∈Peer1，t2∈Peer1，且t1=t2∧λ1(t1)=!m∧λ2(t2)=?m，则称CP=(P1∪P2,T1∪T2,F1∪F2,R1∪R2,MT1∪MT2,M1∪M2,λ)为Peer1和Peer2的同步并发组合，其中λ:T1∪T2→MT1∪MT2。

4.2 同步通信下编排的可实现性

同步通信下检测编排的可实现性可通过3步实现：①通过同步并发组合，得到同步通信下的编排实现，具体参见定义10；②生成编排的可达图和编排实现的可达图；③检测第②步生成的两个可达图是否满足强互模拟关系，若满足，则该编排在同步通信下是可实现的。

定义10同步通信下的编排实现。CPs=(Peer1‖sPeer2‖s…‖sPeern)为同步通信下的编排实现，其中：Peeri表示参与者i，‖s表示同步并发组合。

对于图4所示的4个参与者，经同步并发组合构建的编排实现如图6所示。需要说明的是，图6所示的编排实现是删除隐式库所后得到的。

一旦得到编排实现，便可使用PIPE生成图2所示编排和图6所示编排实现的可达图，分别如图7a和图7b所示。

由于图7a所示可达图和图7b所示可达图不满足强互模拟关系。在同步通信下该编排是不可实现的。

4.3 异步并发组合

本质上，异步通信是非阻塞模式，它是指发送者发出消息后，不等接收者发回响应消息，接着发送下一个消息的通信方式。在异步通信下，发送者在任意时刻都可以发送消息，但前提是接收者已做好了接收消息的准备。与同步通信相比，异步通信要求为每个接收者配备消息缓冲区，以时刻存储需要接收的消息。

图8给出了使用交互式Petri网实现异步通信的思路：

(1)为每个参与者都配备了一个消息缓冲区，用来存储需要接收的消息。在图8中，虚线圆圈表示消息缓冲区，其中，第1个和第2个虚线圆圈表示PeerB的消息缓冲区，第3个和第4个虚线圆圈表示PeerA的消息缓冲区。

(2)消息缓冲区存储的消息类型可通过设置不同的库所来实现。例如，对PeerA而言，其缓冲区由库所m3_buffer和库所m4_buffer实现，其中：m3_buffer用于存储接收消息“m3”，m4_buffer用于存储接收消息“m4”。

(3)消息缓冲区的长度可通过设置库所的容量来实现。例如，对PeerA而言，若库所m3_buffer和库所m4_buffer的容量设置为1，则该参与者消息缓冲区的容量为2。

(4)消息缓冲区中消息的个数可通过设置库所中存放的托肯来实现，但不区分消息的顺序。需要说明的是，与现有文献[6,9,13-18]通过先进先出队列实现的消息缓冲区要求消息先进先出相比，本文实现的消息缓冲区是从库所中取消息，不区分消息的顺序。

对PeerA而言，当PeerA向PeerB发送消息m1(变迁“!m1”发生点火，并向PeerB的消息缓冲区库所m1_buffer中增加一个托肯)后，无需等待PeerB的响应，便可继续向PeerB发送消息m2。对PeerB而言，当库所m1_buffer中有托肯时，PeerB便可接收消息m1(变迁“?m1”发生点火，从m1_buffer中消耗一个托肯)。

异步并发组合是指在异步通信环境下，将多个参与者并发组合为编排实现。下面给出异步并发组合的定义。

定义11异步并发组合。设Peeri=(Pi,Ti,Fi,Ri,MTi,Mi,λi)(i=1,2)是两个参与者，其中，存在m∈MT1∩MT2，t1∈Peer1，t2∈Peer1，且t1=t2∧λ1(t1)=!m∧λ2(t2)=?m，则称CP=(P1∪P2∪{pm},T1∪T2,F1∪F2∪{(t1,pm),(pm,t2)},R1∪R2,MT1∪MT2,M1∪M2,λ)为IPN1和IPN2的异步并发组合，其中λ:T1∪T2λ1(T1))∪λ2(T2)∪{τ}。

4.4 有界异步通信下编排的可实现性

有界异步通信下检测编排的可实现性可通过3步实现：①通过异步并发组合，得到异步通信下的编排实现，具体参见定义12；②生成编排的可达图和编排实现的可达图；③检测第②步生成的两个可达图是否满足弱互模拟关系，若满足，则该编排在异步通信下是可实现的。

需要注意的是，若参与者配置的消息缓冲区的容量为无界，则异步通信下编排实现的可达状态有可能是无界的，无法生成可达图，从而无法分析编排的可实现性。因此，本文所提方法关注有界异步通信编排的可实现性分析，即消息缓冲区的容量为有界的。

定义12异步通信下的编排实现。CPas=(Peer1‖asPeer2‖as…‖asPeern,)为异步通信下的编排实现，其中：Peeri表示参与者i，‖as表示异步并发组合。

对于图3所示的4个参与者，经异步并发组合构建的编排实现如图9所示。在图9中，虚线部分是新增的库所和流关系。

同样地，使用PIPE生成图2所示编排和图9所示编排实现的可达图，分别如图10a和图10b所示。需要说明的是，编排实现的可达图有23个状态和30条弧，图10b只给出了可达图的部分。此外，在图10b中，编排实现中的接收消息动作被映射为τ。因为接收消息动作表示参与者从消息缓冲区中取出消息，属于局部动作，所以是不可见的。

由于图10a所示可达图和图10b所示可达图不满足弱互模拟关系，在异步通信下该编排也是不可实现的。

5 工具实现和实验结果

5.1 工具实现

本文所提方法由工具完全支持，如图11所示。一方面，在PIPE工具的支持下，编排建模人员可使用PIPE直接建模编排，并将编排保存为基于可扩展标记语言(eXtensible Markup Language, XML)格式的PNML文件(Petri Net Markup Language)[18]。PNML是存储Petri网模型的标准文件格式，可被多个Petri网的建模和分析工具支持。此外，还可通过PIPE工具生成编排和编排实现的可达图，并将可达图保存为TXT文件。另一方面，在PIPE源代码的基础上，使用Java语言开发了Generator、Composer和Simulator三个模块。其中:Generator用于实现编排到参与者的映射生成，其输入是PNML文件，输出也是PNML文件；Composer用于实现在同步通信和异步通信下把参与者并发组合为编排实现，其输入是PNML文件，输出也是PNML文件；Simulator用于实现行为等价检测，其输入是TXT文件，输出是等价或不等价。

5.2 实验结果

使用本文方法对来自文献[5-6,8,13,18,20-22,24]中的10案例进行编排可实现性分析。笔记本电脑软/硬件配置如下：内存8 G；操作系统：Win10家庭版X64位；处理器：Intel(R)Core(TM)i7-7700HQ CPU 2.80 GHz；JDK：1.8.0_161；PIPE：4.3.0;开发工具：Eclipse Java Oxygen.2 Release(4.7.2)。

表1给出了实验结果。表中给出了每个案例的名字及来自的文献、参与者的数量、参与者间消息交互的数量，同步通信下编排实现(CPs)的可达图中弧的数量(|A|)和状态的数量(|S|)，异步通信下编排实现(CPas)的可达图中弧的数量(|A|)和状态的数量(|S|)及可实现性分析结果(同步通信下的可实现性分析结果、生成同步通信下编排实现可达图的时间、两个可达图行为等价检测的时间、异步通信下的可实现性分析结果、生成异步通信下编排实现可达图的时间、两个可达图行为等价检测的时间)。“×”表示不可实现，“√”表示可实现，“?”表示无法判定。需要注意的是，在案例2中，由于异步通信下编排实现的可达图的状态数为无界，记为“unbounded”，在异步通信下无法分析编排的可实现性。表中只记录了生成具有20 000个状态的可达图需要的时间为331 s。

使用本文所提方法对表1所示10个案例进行可实现性分析的结果与案例所在文献给出的可实现性分析结果一样，从而说明了本文所提方法的有效性。

表1 实验结果

6 结束语

本文使用Petri网提出一种分析编排可实现性的方法，该方法能自动将编排生成为参与者，并从行为等价的角度，在同步通信和有界异步通信下，检测编排的可实现性。下一步工作的重点是对无界异步通信下编排的可实现性进行分析。