祝 义，黄志球，周 航

1.南京航空航天大学 计算机科学与技术学院，南京 210016

2.江苏师范大学 计算机科学与技术学院，江苏 徐州 221116

1 引言

面向服务的计算（service oriented computing）是互联网上典型的分布式计算应用。在过去20年里，Web服务组合已经成为应用集成与互操作研究与开发中最活跃的领域之一。WS-BPEL（Web services business process execution language）是由OASIS组织为了规约Web服务中业务流程行为提出的标准执行语言。尽管已经对BPEL模型展开深入研究，然而其可靠性、普适性、个体性等仍需要被讨论，尤其是诸如云计算、社交网络以及物联网技术迅速发展后，人们对BPEL模型的可靠性要求越来越高，如何进一步提高复杂BPEL模型的可靠性已经成为一个关键问题[1]。

形式化方法，源于Dijkstra和Hoare的程序验证，其主要优点是具有精确性，可以验证，并且便于机器支撑和自动处理等。这些特点对克服目前复杂BPEL模型的可靠性差，难以实现自动化的困境具有明显的作用。进程代数是一种用来解决并发系统通信问题的形式化方法，可以描述和分析并发、异步、非确定等系统行为，具有良好的语义与可扩展性，使得它非常适合于BPEL模型的建模与分析。通信顺序进程（communicating sequential process，CSP）是Hoare[2]在1978年提出的一种能够对并发系统进行模型检测的进程代数方法。CSPM是一种基于CSP的惰性函数式程序语言，可用于机器执行。FDR（failure divergence refinement）是一种基于CSPM描述的分析程序工具，牛津大学于2016年发布了最新版本FDR3.4[3]。

WS-BPEL结合了XLANG[4]和WSFL（Web services flow language）[5]的特征，可以建模多个服务共同参与的业务流程行为。WS-BPEL通过抽象业务流程和可执行业务流程来描述Web服务，其入口和出口信息通过唯一的Web服务接口来定义。其中，抽象业务流程描述业务流程中单个服务的接口行为，可执行业务流程描述业务流程中服务之间的交互以及业务流程的内部逻辑。

为了让Web服务能够组合在一起并顺利执行，需要对来自不同组织的Web服务进行分析与验证，主要是保证服务组合在执行过程中不会出现死锁或冲突。这种分析与验证工作主要包含三方面[6]：语法相容性、语义相容性以及行为相容性。其中，语法相容性是指各成员服务的交互接口应该是一致的，WSDL（Web services description language）已为Web服务提供了标准的接口规约方法；语义相容性是指各成员服务之间交互的信息应该是精确的、无二义的；行为相容性是指各成员服务应该在操作的执行上达成一致。当前很多研究工作者针对Web服务组合验证开展了很多工作，一般都是基于某种形式化方法，例如通过进程代数、Petri网或自动机对Web服务组合建模，然后在形式化模型中进行分析与验证。但是这些方法大多数不具备程序设计能力，因此直接通过形式化方法描述的Web服务组合很难在实践中得以推广。

本文贡献在于将CSPM与BPEL进行了深度结合。首先在语言层次上建立BPEL到CSPM的映射，这样能够将通过BPEL建立的模型映射为CSPM模型；然后通过模型检测工具FDR对CSPM模型的活性、安全性、确定性和无死锁性分别进行模型检测；最后将CSPM模型检测的结果用于BPEL模型的修改，这样能够在很大程度上提高BPEL模型的可靠性。

本文组织结构如下：第2章提出了基于CSPM的BPEL模型建模与验证框架；第3章给出了CSPM的进程代数定义；第4章详细描述了BPEL到CSPM的映射方法；第5章以一个在线购物系统为例，讨论了本文方法的使用效果；第6章进行相关工作比较；第7章总结全文并给出结论。

2 基于CSPM的BPEL模型建模与验证框架

为了从根本上提高BPEL建模的可靠性，本文建立了基于CSPM的BPEL模型建模与验证框架。如图1所示。

Fig.1 Framework for modeling and verifying BPEL model based on CSPM图1 基于CSPM的BPEL模型建模与验证框架

该框架主要包含以下基本步骤：第1步在语言层次上建立BPEL到CSPM的映射机制，实现BPEL模型到CSPM模型的转换；第2步将转换得到的CSPM模型输入到模型检测工具FDR，保存为扩展名为.csp的模型文件，即实现（implementation），为进一步模型检测做好准备；第3步根据要检查的BPEL模型性质建立CSPM断言，即规约（specification），例如安全性、活性、确定性和无死锁性断言；第4步将CSPM断言逐个输入到FDR进行模型检测，如果正确，就表明该断言通过模型检测，如果错误，FDR则输出反例，反例通过比较规约行为迹与实现行为迹来找出进程中的错误；第5步根据反例对CSPM模型（实现）进行修改，并重新输入到FDR中进行模型检测，如此循环，直至所有CSPM断言（规约）都验证通过；第6步根据模型检测结果对BPEL模型进行修改，得到可信BPEL模型。

3 CSPM的进程代数定义

CSPM是基于CSP的惰性函数式编程语言，因此下面主要讨论Web服务与CSP之间的关系。将Web服务映射为进程，并将Web服务的每条指令映射为进程中的事件，那么Web服务的组合特征表现为进程的并发特征。

定义1（通信顺序进程）一个通信顺序进程CSP可定义为：

Σ={a0,a1,…,an-1}是可观察事件集合，ai∈Σ，0≤i＜n-1，A∈PΣ，PΣ为Σ的幂集；X是进程变量。定义解释如下：

STOP：停止，表示进程不与外界发生任何通信，通常表示进程死锁或不收敛；

SKIP：跳过，表示进程不做任何事情直到最后停止；

a→P：前缀操作，表示事件a执行后执行进程P；

P;Q：顺序复合，表示进程P执行后执行进程Q；

P＜expr＞Q：条件复合，表示expr表达式为真时执行进程P，否则执行进程Q；

P□Q：外部选择，表示执行进程P或Q依赖于进程执行的第一个事件；

P||Q：同步并发，P仅能执行α(P)中的事件，Q仅能执行α(Q)中的事件，α(P)⋂α(Q)的事件P与Q同步执行；

μX·F(X)：X是一个进程变量，F(X)是包含X的前缀表达式，该递归方程具有事件集A上的唯一解，其中A=αX。

此外，CSP提供通道表示一类事件的集合，例如channel a：Int，表示通道a能够与任何带有整型数据的事件通信，事件a.1是通道a声明的一个元素。

4 BPEL语言到CSPM语言的映射方法

为了验证BPEL模型的相关性质，首先要建立BPEL语言到CSPM语言的映射机制，实现BPEL模型到CSPM模型的转换。在WS-BPEL2.0规约中，receive、reply、invoke、sequence、switch、pick、while和 flow 是描述BPEL控制逻辑的关键元素。本文主要关注Web服务行为的控制逻辑方面，因此不考虑BPEL中的 compensation、fault handler、assign、correlation set、link condition和variables等元素。下面介绍BPEL语言到CSPM语言的映射方法。

4.1 基本活动映射

（1）invoke活动

invoke活动主要用来获取伙伴服务所提供的功能，它通过操作向伙伴服务发送服务调用消息。invoke活动分为单向调用和请求回复调用两种类型。单向invoke活动只向伙伴服务发送服务调用请求，而不需回复，但是请求回复调用除了发送请求外同时还需回复。单向invoke活动的映射过程是将发送的请求对应到CSP的一个输出动作。具体映射关系如图2所示。

Fig.2 Mapping from action one-wayinvoketo CSP图2 单向invoke活动到CSP的映射

对于请求回复invoke活动，将请求和回复消息分别对应到CSP的输出和输入活动，具体映射关系如图3所示。

Fig.3 Mapping from action request-replyinvoketo CSP图3 请求回复invoke活动到CSP的映射

单向invoke活动在CSPM中表示为op!message➝P。双向invoke活动在CSPM中表示为op!message1➝op?message2➝P。

（2）receive活动

receive活动主要是用户接受伙伴服务的消息调用。它的映射规则是，将receive活动接受的消息对应到CSP的一个输入动作。具体映射关系如图4所示。

Fig.4 Mapping from actionreceiveto CSP图4 receive活动到CSP的映射

receive活动在CSPM中表示为op?message➝P。

（3）reply活动

reply活动主要对先前接受的receive活动发送相应的请求响应。它的转换规则是，将reply活动发送的消息对应到CSP的一个输出动作。具体映射关系如图5所示。

Fig.5 Mapping from actionreplyto CSP图5 reply活动到CSP的映射

reply活动在CSPM中表示为op!message➝P。

4.2 组合活动映射

（1）sequence活动

sequence活动主要用于表示子活动之间的顺序结构的控制流关系。它的映射规则是，将前面一个活动的进程P1中的阻塞状态和后面一个活动的进程P2中的初始状态融合成一个状态，从而将两个进程“串行”地联接成一个进程，多个进程的顺序结构依此类推。其中，Pi为执行完第i个子活动acti的系统后继进程，i∈N且1≤i≤n。具体映射关系如图6所示。

当αP={act}时，即子活动为原子活动时，上述进程表达式简化为：

Fig.6 Mapping from actionsequenceto CSP图6 sequence活动到CSP的映射

sequence活动在CSPM中可表示如下：

（2）switch活动

switch活动主要用于控制分支条件选择，当执行某个活动的前提条件得到满足时，该活动就被选择，等到该活动执行完毕，switch活动结束。switch活动的映射过程是，首先获得待选择的各分支活动的进程P1,P2,…,Pn，然后将各分支进程的初始状态融合为一个统一的初始状态，同时将各分支进程的阻塞状态融合为一个统一的阻塞状态。具体映射关系如图7所示。

Fig.7 Mapping from actionswitchto CSP图7 switch活动到CSP的映射

switch活动在CSPM中可表示为：

（3）while活动

while活动定义了一种典型循环结构，只要条件为真，指定活动就反复执行，直到条件为假时while活动才结束。while活动的转换过程是，首先获得指定活动的进程，接着将该进程中指向阻塞状态的迁移都改为指向初始状态，最后再添加一个从初始状态转换到阻塞状态的迁移，该迁移表示为一个空操作。具体映射关系如图8所示。

Fig.8 Mapping from actionwhileto CSP图8 while活动到CSP的映射

while活动在CSPM中表示为：

（4）pick活动

pick活动包含若干个onMessage元素，它等待特定的消息到达，当最先收到某个消息时，就触发该消息对应的活动，当该活动执行完毕后，pick活动结束。pick活动的转换过程是，首先将触发每个活动所对应的消息看作一个receive活动，然后再将它们融合成一个顺序执行活动。最后将各顺序活动融合成一个分支选择活动。具体映射关系如图9所示。

pick活动在CSPM中表示为：

（5）flow活动

Fig.9 Mapping from actionpickto CSP图9 pick活动到CSP的映射

Fig.10 Mapping from actionflowto CSP图10 flow活动到CSP的映射

flow活动主要用于表示各个子活动的并发执行，可以用CSP中并发操作符来表示。具体映射关系如图10所示。

flow活动在CSPM中表示为：

目前，已经通过基于MDE（model driven engineering）[7]的AMMA（ATLAS model management architecture）[8]平台初步完成了原型系统设计。AMMA开发平台为法国ATLAS（Atlantic data systems）研究组设计的通用模型转换平台，平台的模型转换语言ATL（ATLAS transformation language）是AMMA平台的一部分，它是一种模型转换语言和工具集，提供了从源模型产生目标模型的方法。ATL在Eclipse平台上的集成开发环境（integrated development environment，IDE）提供了标准的用于模型转换的开发工具。首先，基于AMMA平台的KM3元模型体系，通过元建模构造BPEL元模型和CSP元模型；其次，利用ATL针对BPEL元模型和CSP元模型构造转换规则，通过将对应的实例模型进行相互转换，实现在MDE下BPEL模型到CSP模型的转换；最后，通过建立模型到文本的转换将CSP模型转换为CSPM代码，CSPM代码可以直接导入到FDR工具中编译执行。

5 实例

一个在线购物（online shopping）应用共涉及顾客（Buyer）、售货商（Seller）、银行（Banker）、邮局（Postoffice）和快递公司（Shipper）5个协作服务。交易之初，Buyer向Seller发送订单请求消息（ordreq），Seller接收到ordreq后，向Banker发送货款支付请求消息（payreq），如果Buyer的银行卡可用额度能够支付所定货物，则Banker向Seller返回支付成功消息（payok），否则返回支付失败消息（payfail）。当Seller收到payok，则选择Postoffice或者Shipper向Buyer发送货物（postreq/shipreq），货物发送完成后（postend/shipend），Seller再通知Buyer货物运送完成(postsucc/shipsucc）。如果Buyer的银行卡可用额度不能支付所定货物，则Seller拒绝Buyer的本次订单（rejection）。在线购物为了完成共同的业务目标，它们共享数据，通过发送和接收消息向合作伙伴请求并提供服务。通过以上分析，首先通过BPEL对该组合服务建模，如图11所示。

Fig.11 BPEL model of online shopping图11 在线购物BPEL模型

然后将建模结果通过第3章介绍的映射方法进行映射，得到的在线购物CSP模型表示如下：由于在CSPM中进程必须要标准化（normalize），因此OS（online shopping）进程按阶段被划分为BS（Buyer-Seller）、BSB（Buyer-Seller-Banker）、BSBS（Buyer-Seller-Banker-Shipper）以及BSBP（Buyer-Seller-Banker-Postoffice）4个进程，上述CSP在CSPM中代码如下：

将上述CSPM代码存为OnlineShoping.csp文件并通过FDR3打开，接下来通过FDR3分别对其安全性、活性、确定性以及无死锁性进行模型检测。在FDR3中建立的CSPM断言以及模型检测结果如下。

（1）安全性

以上断言表示进程BS、BSB、BSBS、BSBP迹精化于进程OS，即trace(BS)⊆trace(OS)、trace(BSB)⊆trace(OS)、trace(BSBS)⊆trace(OS)、trace(BSBP)⊆ trace(OS)。模型检测结果如图12所示。

（2）活性

该断言表示进程BS、BSB、BSBS、BSBP失效/发散精化于进程OS，即failures(BS)⊆failures(OS)且divergences(BS)⊆divergences(OS)，failures(BSB)⊆failures(OS)且 divergences(BSB)⊆divergences(OS)，failures(BSBS)⊆failures(OS)且 divergences(BSBS)⊆divergences(OS)，failures(BSBP)⊆ failures(OS)且 divergences(BSBP)⊆divergences(OS)。模型检测结果如图13所示。

（3）确定性

Fig.12 Safety checking of online shopping图12 在线购物系统安全性检测结果

Fig.13 Liveness checking of online shopping图13 在线购物系统活性检测结果

该断言表示进程BS、BSB、BSBS、BSBP、OS都不会发散，不会出现任何既可接受又可拒绝的行为选择。例如对于进程OS而言，OS是确定性进程表明divergences(OS)={}并且 s^＜a＞∈trace(OS)⇒(s,{a})∉failures(OS)。模型检测结果如图14所示。

（4）无死锁性

该断言表示进程BS、BSB、BSBS、BSBP、OS都无死锁。例如对于进程OS而言，OS无死锁表明对于任意迹s而言，(s,∑)∉failures(OS)。模型检测结果如图15所示。

以上实验结果显示所有进程都通过了FDR模型检测，表明在线购物系统CSPM模型具有极高的可靠性。接下来根据模型检测结果对BPEL模型进行修改，最后可以得到高可信的BPEL模型。

另外，还可以根据图1中反例生成原理检查系统单个行为以及组合行为的正确性。

（1）单个行为的正确性

假设Seller没有收到Banker确认的payok消息，就可以选择Postoffice或者Shipper向Buyer发送货物（postreq/shipreq）。

在FDR中对SELLER进程进行相应的修改：

Fig.15 Deadlock freedom checking of online shopping图15 在线购物系统无死锁性检测结果

编译执行后发现断言assert OS[T=BS，就不能通过模型检测，通过Debug可以看到FDR产生的反例。BS进程在执行ordreq后可接受事件为payreq，但OS进程在执行ordreq后拒绝除了payok之外的所有事件，进程进入死锁状态。反例说明SELLER只有在收到Banker发来的payok之后才能发货，否则系统就会因为没有可同步的事件进入死锁状态。

（2）组合行为的正确性

假设Shipper或者Postoffice是并行关系。在FDR中对OS进程修改如下：

OS=BSBS[|{||}|]BSBP

编译执行后发现断言assert OS[FD=BS没有通过模型检测，通过Debug可以看到FDR产生的反例。BS进程在执行ordreq后可接受事件为payreq，OS进程在执行ordreq后可接受事件为payreq和ordreq，但BS进程拒绝连续执行两次ordreq，因此进程进入死锁状态。反例说明OS进程在收到Buyer的订单请求ordreq后没有经过任何处理可以再次接受订单请求，这与实际情况不符。出现这一状况的原因是BSBS进程与BSBP进程是并行关系，也就是说既可以选择Shipper，也可以选择Postoffice运送货物，因此OS进程允许连续执行两次ordreq，而实际情况只能选择Shipper和Postoffice两者之一运送货物，因此BSBS与BSBP不能是并行关系，必须是选择关系。

参照以上反例产生的过程，能够检查系统其他行为的正确性，由于篇幅原因，此处不再赘述。

6 相关工作比较

目前关于BPEL业务流程形式化建模与验证代表性的工作包括以下三方面：

（1）直接使用进程代数描述与验证BPEL业务流程的相关性质。文献[9]通过进程演算建模Web服务的编排与编制，将进程演算中互模拟的方法用于检验编排与编制之间的一致性。文献[10]提出了一种代价概率进程代数（priced probabilistic process algebra，PPPA），并给出了基于PPPA统一建模和分析Web服务组合功能和QoS的方法。文献[11]通过转换WSCI（Web service choreography interface）标准到CCS来进行Web服务编排分析，并分析了参与编排的服务交互行为的相容性和可替换性，对于不相容的服务提供适配器实现通信。文献[12]将任务映射为进程，任务间的连接映射为通道，通过Pi演算对Web服务之间的交互行为进行建模。

（2）直接使用自动机描述与验证BPEL业务流程的相关性质。文献[13-14]使用卫式自动机（guarded automata）对Web服务的BPEL流程进行建模，将服务组合看作服务之间通过异步消息传递的全局会话协议，并将会话协议的同步条件以及系统目标属性用线性时序逻辑（linear temporal logic，LTL）描述，然后通过模型检验工具SPIN进行验证。文献[15]利用有限状态机分别对Web服务和编排进行建模，使用有向图描述Web服务的证书暴露策略，并通过匹配证书暴露以及访问控制策略来验证编排的所有可能会话。文献[16]利用时间自动机对带时间约束的Web服务行为进行建模，并在此基础上分析了服务之间以及服务与规约之间的时间行为相容性和可替换性。

（3）直接使用Petri网描述与验证BPEL业务流程的相关性质。文献[17]提出了一种基于服务簇的服务组合方法，并应用逻辑Petri网对其进行形式化建模描述。文献[18]针对如何有效评估服务系统的性能表现，提出了一种基于排队Petri网的性能建模和分析方法。文献[19]针对如何有效发现Web服务组合中性能瓶颈的问题，提出了一种基于随机Petri网的Web服务组合性能分析模型。文献[20]转换抽象BPEL过程到有色Petri网，通过分析交互服务之间的行为相容性，将部分相容的服务进行了自动组合。

上述方法能够描述与验证BPEL业务流程的相关性质，但这些形式化方法不具备程序设计能力，没有从程序语言层次上建立BPEL到形式化模型的映射关系，因此很难从实际应用中判断这些方法的实用价值。与以上研究工作相比，本文在BPEL业务流程建模与验证方面另辟新径：从模型映射的角度来看，基于程序语言层面映射得到的CSPM模型保留了BPEL业务流程的完整语义，因此通过这种方法建立的BPEL模型具有极高的可靠性；从可追踪性的角度来看，因为BPEL与CSPM之间的映射是一对一的，所以BPEL业务流程与CSPM模型之间保持了良好的可追踪性，从而CSPM模型检测结果可以直接用于BPEL业务流程建模与修改。此外，本文工作也为可信软件设计提供了新的思路，给出了一套实践中切实可行的解决方案。

7 总结与展望

本文在研究了BPEL业务流程形式化建模与验证相关工作的基础上，提出了一种基于CSPM的BPEL业务流程建模与验证方法，为提高BPEL业务流程建模可靠性找到一条新的行之有效的途径。主要工作为：给出基于CSPM的BPEL业务流程建模与验证框架；根据BPEL业务流程特征给出了CSPM的进程代数定义；详细描述了BPEL到CSPM的映射方法；通过在线购物系统建模实例说明了该方法如何应用于BPEL业务流程建模与验证。

此外，本文没有考虑BPEL业务流程建模中涉及到的时间、资源、隐私等非功能性质的验证问题，因此进一步工作是在现有研究基础上扩展CSPM的非功能性质，并将其应用于基于进程代数的BPEL业务流程的建模与验证方法中。

[1]Sheng Q Z,Qiao Xiaoqiang,Vasilakos A V,et al.Web services composition:a decade's overview[J].Information Science,2014,280:218-238.

[2]Hoare CAR.Communicating sequential processes[J].Communications of theACM,1978,21(8):666-677.

[3]University of Oxford.fdr3-3702-windows-x86_64.msi[EB/OL].(2016).http://www.cs.ox.ac.uk/projects/fdr/.

[4]Microsoft.Web services for business process design(XLANG)[EB/OL].(2003).http://xml.coverpages.org/xlang.html.

[5]IBM.Web services flow language(WSFL)[EB/OL].(2003).http://xml.coverpages.org/wsfl.html.

[6]Li Xitong,Fan Yushun,Sheng Q Z,et al.APetri net approach to analyzing behavioral compatibility and similarity of Web services[J].IEEE Transactions on Systems,Man and Cybernetics:PartASystem and Humans,2011,41(3):510-521.

[7]Schmidt D C.Guest editor’s introduction:model-driven engineering[J].IEEE Computer,2006,39(2):25-31.

[8]ATLAS Team.ATLAS transformation language(ATL)home page[EB/OL].(2017).http://www.eclipse.org/atl/atlTransformations/.

[9]Ferrara A.Web services:a process algebra approach[C]//Proceedings of the 2nd International Conference on Service Oriented Computing,New York,Nov 15-19,2004.New York:ACM,2004:242-251.

[10]Xiao Fangxiong,Huang Zhiqiu,Cao Zining,et al.Unified formal modeling and analyzing both functionality and QoS of Web services composition[J].Journal of Software,2011,22(11):2698-2715.

[11]Brogi A,Canal C,Pimentel E,et al.Formalizing Web service choreographies[J].Electronic Notes in Theoretical Computer Science,2004,105:73-94.

[12]Kazhamiakin R,Pistore M.Choreography conformance analysis:asynchronous communications and information alignment[C]//LNCS 4184:Proceedings of the 3rd International Workshop on Web Services and Formal Methods,Vienna,Sep 8-9,2006.Berlin,Heidelberg:Springer,2006:227-241.

[13]Fu Xiang,Bultan T,Su Jianwen.Analysis of interacting BPEL Web services[C]//Proceedings of the 13th International Conference on World Wide Web,New York,May 17-20,2004.New York:ACM,2004:621-630.

[14]Fu Xiang,Bultan T,Su Jianwen.Synchronizability of conversations among Web services[J].IEEE Transactions on Software Engineering,2005,31(12):1042-1055.

[15]Paci F,Ouzzani M,Mecella M.Verification of access control requirements in Web services choreography[C]//Proceedings of the 2008 International Conference on Services Computing,Honolulu,Jul 8-11,2008.Washington:IEEE Computer Society,2008:5-12.

[16]Ponge J,Benatallah B,Casati F,et al.Analysis and applications of timed service protocols[J].ACM Transactions on Software Engineering and Methodology,2010,19(4):1-38.

[17]Wu Hongyue,Du Yuyue.A logical Petri net-based approach for Web service cluster composition[J].Chinese Journal of Computers,2015,38(1):204-218.

[18]Gu Jun,Luo Junzhou,Cao Jiuxin,et al.Performance modeling and analysis of service systems using queueing Petri nets[J].Chinese Journal of Computers,2011,34(12):2435-2455.

[19]He Yanxiang,Shen Hua.A stochastic Petri net-based performance bottleneck location strategy for Web services composition[J].Chinese Journal of Computers,2013,36(10):1953-1966.

[20]Tan Wei,Fan Yushun,Zhou Mengchu.A Petri net-based method for compatibility analysis and composition of Web services in business process execution language[J].IEEE Transactions on Automation Science and Engineering,2009,6(1):94-106.

附中文参考文献：

[10]肖芳雄,黄志球,曹子宁,等.Web服务组合功能与QoS的形式化统一建模和分析[J].软件学报,2011,22(11):2698-2715.

[17]吴洪越,杜玉越.一种基于逻辑Petri网的Web服务簇组合方法[J].计算机学报,2015,38(1):204-218.

[18]顾军,罗军舟,曹玖新,等.基于排队Petri网的服务系统性能建模与分析方法[J].计算机学报,2011,34(12):2435-2455.

[19]何炎祥,沈华.一种基于随机Petri网的Web服务组合性能瓶颈定位策略[J].计算机学报,2013,36(10):1953-1966.