陈莹1，邢建春1，王洪达1，杨启亮1,2

　　（1.解放军理工大学 国防工程学院，江苏 南京 210007；2.南京大学 计算机软件新技术国家重点实验室，江苏 南京 210093）

      摘要：针对BPEL过程在死路径消除语义下建模与分析不够完善的问题，提出了一种新的BPEL过程建模与分析方法。该方法建立了将BPEL死路径消除语义转化为普通if-then-else的规则，进而可以利用着色Petri网（CPN）形式化地对BPEL过程进行建模，并通过CPNTools对BPEL过程的建模进行自动分析及验证。案例分析表明，该方法具有一定的实用性和可行性，能够帮助软件工程人员更好地测试、调试和维护BPEL程序。

　　关键词：Web服务组合；BPEL程序依赖图；死路径语义消除；着色Petri网

　　中图分类号：TP311.5文献标识码：ADOI： 10.19358/j.issn.1674-7720.2017.06.008

　　引用格式：陈莹，邢建春，王洪达，等. 死路径消除语义下的BPEL过程建模与分析［J］.微型机与应用，2017,36（6）：22-25.

0引言

　　*基金项目：江苏省自然科学基金项目（BK20151451）Web服务业务过程执行语言（BPEL或者WSBPEL）是为满足基于服务的业务流程需要而制定的业界事实标准［1］。基于BPEL的组合Web服务因其能够提供功能更加强大的服务而受到业界的广泛认可［2］。然而，服务业务流程并不总是完美的，在流程设计中往往会存在一些问题（比如死路径消除），这很难满足高可靠度和可行性的要求。因此，BPEL过程在死路径消除语义下建模与分析的问题仍然需要完善。所谓死路径消除是指扩大某个不可执行活动的范围以至在该活动执行完成之后执行的所有活动都将无法完成。每个活动都承载着充当下一个活动是否能执行的判定条件的角色。目前，有关BPEL过程建模分析与验证的技术主要有Petri网［3］、进程代数［4］和自动机［5］等方法。从BREUGL F V［6］分析的近100篇论文中发现，采用进程代数和自动机的方法对BPEL过程进行建模，其模型比较复杂抽象，建模过程难度比较大。又由于BPEL程序同时支持并发路径和死路径消除（Dead Path Elimination, DPE），为了最大程度地解决BPEL过程建模的并发路径和死路径消除问题，需对现有的传统建模方法进行改进。

　　基于业务流程的复杂性，使用BPEL流程组合建模比较容易出现错误［7］，并且在语言表达上不够简明易懂。为了使流程语言表达更加准确、简单，需要采用形式化的方法对BPEL过程进行建模与分析。

　　本文基于着色Petri网对BPEL过程在死路径消除语义下进行建模。着色Petri网（Colored Petri Net, CPN）是对一般Petri网的扩展，具有Petri网的所有性质，它将Petri网与程序元语言（Meta Language，ML）结合，并以简洁明了的方式描述并发系统。本文的主要创新点是在已有工作的基础上，提出了一种死路径消除语义下的BPEL过程建模与分析方法，该方法建立了将BPEL死路径消除语义转化为普通ifthenelse的规则，并采用CPNTools工具将其形式化地表现出来。通过案例分析表明，与现有的BPEL过程建模相比，本文提出的BPEL过程在死路径消除语义下的建模更具有实用性和可行性，从而能够帮助软件工程师更好地测试、调试和维护BPEL程序。

1相关概念

　　1.1BPEL简介与死路径消除

　　BPEL是一种使用XML（标准通用标记语言下的一个子集）编写的服务组合编制语言，用于自动化业务流程的形式规约语言，可以协调多个服务的执行。由于业务流程的需要，BPEL提供了基本活动与结构化活动两种不同的活动类型［8］。同时，BPEL使用<flow>来提供并发性，并发活动的同步用<link>表示。

　　一个BPEL活动可以是多个<link>的源活动，这些<link>称为该活动的outgoing links［9］。活动结束时，根据每个<link>对应的变迁条件对<link>状态进行设置（true or false）。如果没有与明确的变迁条件相关联，则默认的变迁条件为真。一个活动同时也可以是多个<link>的目标活动，这些<link>称为该活动的incoming links。关于incoming links状态的变量构成的布尔表达式，定义为BPEL过程融合条件（join condition）。只有当融合条件为真时，活动才可以执行。当所有的<link>取得了某种状态后，这个连接条件的值才能确定下来［10］。如果这个连接条件是真，则活动可以被执行，反之如果连接条件为假，则该活动不能执行并且所有通过它的<link>均被置为假。这样的状态将一直向下传递直到遇到某个活动的变迁条件为真，此时目标活动才可以执行，这种技术称之为死路径消除。

　　1.2CPN简介

　　着色Petri网（Colored Petri Net, CPN）是由丹麦研究员Kurt Jensen于1981年所提出，与大家所熟知的基本Petri网一样，CPN也是由库所、变迁和弧所组成［11］，但不同的是CPN加入了元素声明并且具有对系统进行仿真和验证的能力。CPN结合了基本Petri网和程序语言的优点，可将复杂的业务流程用图形的方式进行建模描述，使得流程变得简单、更易于理解。此外，还可以运用一种强大的着色Petri网仿真工具CPNTools对系统的有界性、活性及其公平性等性质进行验证。本文的案例就是运用了此工具进行仿真、验证和分析，从而证实了文中所提出规则的准确性。

　　定义［9］：一个CPN是由一个九元组 CPN=(∑, P,T,A,N,C,G,E,I)所组成的。式中：

　　∑表示颜色（Color）的非空有限集合；

　　P：描述系统库所（Place）的有限集合；

　　T：变迁（Transition）的有限集合；

　　A：弧（Arc）的有限集合，满足P∩T=P∩A=A∩T=；

　　N：A→（P×T∪T×P）为节点（Node）函数；

　　C：（P∪T）→∑ss为颜色函数，其中∑ss为∑的有限子集；

　　G：T→表达式为T的守卫函数，即∨t∈T，［Type(G(t))=B∧Type(Var(G(t)))∑］，其中Type(v)表示变量v的类型，Var（exp r）表示表达式exp r中的变量集合；

　　E：A→表达式是弧表达式函数，形如∨a∈A，［Type(E(a))=C(P(a))ms∧Type(Var(E(a)))∑］;

　　I：P→表达式的初始标示，形如∨p∈P，［Type(I(p))=C(P)ms］。

　　2DPE语义下的BPEL过程建模中的转换规则

　　关于BEPL到Petri网的映射规则，早在2004年德国柏林Humboldt University的HINZ S等提出了一套完整的BPEL到Petri网转化规则［12］。而且STAHL C还在他的硕士毕业论文中提到了死路径消除语义下的建模规则，为消除死路径模型，他们建立了一个链接模式，嵌入一个活动［12］。而本文的贡献主要是提出一种将BPEL死路径消除语义转化为普通ifthenelse的规则，并将其形式化的表述出来。

　　在BPEL中，将<link>活动看作一项基本活动，把它的连接条件看作是这个活动的决定性条件。根据<link>活动和DPE语义，有如下四条规则可以覆盖所有的情况。

　　其中定义3个颜色集：

　　colset E=with e; colset L=bool;

　　colset ACTIVE=product L×E;

　　9个变量：

　　var l，lA，lB，l1，l2，l3，jc，ran：L，a：E。

　　2个函数：

　　fun OK (l1：L) = (l1 = true)；

　　fun Skip(l1：L) = (l1 = false)。

　　规则 1：单连接。如图1所示，Activity A、Activity B、Activity C分别表示三个基本活动，而且这三个活动都在活动<flow>中。箭头线表示两个活动之间的控制流，加粗线表示<link>活动。Activity B的变迁条件是tc1，Activity B的连接条件是一个默认值为真。根据DPE语义，单<link>连接的转换规则可以用图2来说明。在这个转换中，将<link>转化为正常的控制流结点并且活动表示为l1=tc1。因此可用传统的分析方法来分析BPEL程序的路径可行性。

　　图1中的活动网中，库所Start Activity A表示活动A的初始状态，其颜色集为ACTIVE。当托肯值是(true，e)时，表示活动A能正常运行，根据弧表达式的运算，触发变迁Activity B，使得其中一个case语句被执行，其他语句被跳过，表示活动B正常运行［9］。另一方面，当托肯值为（false，e）时，则会触发变迁Skipping B，表示活动B被跳过。库所Finish Activity C的托肯值表示活动最终的状态，即活动是否正常执行。

　　规则2：两个相连的<link>。如有两个<link>相继连接，可用图2来表示转换规则。

　　规则 3：一个<link>有两个后继<link>。如果一个<link>后面有两个后继<link>，则转换规则如图3所示。

　　规则4：一个<link>的源活动中包含一个谓词活动（<while>，<if>，<pick>）。如果一个<link>的源活动中包含一个断言式结构，则转换规则如图4所示。图中，活动F的执行与否取决于谓词活动（例如<if>），因此，活动l1表示l1=if(if表示谓词活动的决定条件)。

　　由于规则2至规则4活动网的运行规则与规则1相似，限于篇幅，此处不再赘述。

　　以上4个规则中，每个目标活动的<link>是一个基本活动，如果目标活动是一个结构活动，活动包括它本身也将被忽略。同时将一直应用这4个规则，直到BPEL程序中不再有这种结构。

3案例分析

　　3.1案例描述

　　在本节中，采用了WSBPEL 2.0Primer［1］的例子来评估此方法。在图5的示例中，四个活动是并发执行的。<flow>活动开始时，四个活动同时开始执行。由于<link>的变迁条件是完全相反的（大于或等于5 000），这意味着两个后继活动approve Credit或decline Credit中只有一个将被执行。

　　在设计BPEL控制流图时，当没有考虑DPE的控制流图的情况时，有些死锁等问题是检测不出来的。而当考虑了DPE后，这些死锁问题就可以被检测出来。因此，死路径消除语义下的BPEL过程建模与分析是很有必要的。

　　3.2建模与分析

　　根据BPEL流程的CPN映射规则进行建模，整个案例是由两个flow活动、一个switch活动和High Risk、Low Risk、Reply以及Invoke四个基本活动所组成。其中，flow活动由库所Begin Flow和库所End Flow之间的部分所组成，switch活动由库所Begin Switch和库所End Switch之间的部分所组成，限于篇幅，案例图略。

　　对于以上案例的CPN模型，运用CPNTools的状态空间分析工具对模型的性质进行自动验证，图6是描述活动性质的数据，从图中可看出，模型中不存在死标识，也不存在不可发生的变迁，也就是说全部变迁都是活性的，因此整个案例模型满足活性性质的要求，从而验证了案例的合理性。

4结束语

　　本文基于BPEL控制流图（考虑了并发结构和DPE语图4包含谓词活动的转换示意图图5一个典型的程序义），提出了一种新的分析BPEL过程路径可行性方法，主要贡献分为两个方面。第一，一个新型的BPEL控制流图，即一个控制流图能抽象出WSBPEL程序的执行过程并考虑了死路径消除语义。第二，应用CPNTools工具，将复杂的BPEL控制流图转换为较简单明了的流图，并运用CPN中状态空间分析工具对其进行有界性、活性等分析，从而验证了方法的可行性。

参考文献

　　［1］ Wang Hongda, Xing Jianchun, Yang Qiliang,et al. Optimal control based regression test selection for service-oriented workflow applications［J］. Journal of Systems & Software, 2016, 124:274-288.

　　［2］ 郑剑，江建慧. Web服务软件测试技术进展［J］. 计算机应用与软件，2009，26（10）：101-104.

　　［3］ HINZ S，SCHMIDT K，STAHL C. Transforming BPEL to Petri Nets［C］.Proceeding of the 3rd International Conference on Business Process Management (BPM 2005)， Berlin，2005: 220235.［4］ FERRARA A. Web services: a process algebra approach［C］. Proceedings of the 2nd Internationa Couference on Service Oriented Computing. New York: ACM Press, 2004：242-251.

　　［5］ FOSTER H, UCHITEL S, MAGEE J, et al. Modelbased verification of Web service compositions［C］.

　　Proceedings of the 18th IEEE International Conference on Automated Software Engineering, 2003：152-161.

　　［6］ BREUGEL F V, KOSHKINA M. Models and verification of BPEL［EB/OL］.（200609xx）［2016-10-19］http://www.cse.yorku.ca/~franck/research/drafts/tutorial.pdf. September 2006.

　　［7］ OUYANG C, BREUTAL S. WofBPEL: a tool for automaed analysis of BPEL processes ［J］. Lecture Notes in Computer Science，2005，3826: 484489.

　　［8］ 余港. BPEL中基于异步模式的人工任务执行系统的研究与实现［D］. 重庆:重庆大学，2010.

　　［9］ STAHL C. Transformation von BPEL4WS in Petrinetze［D］. Berlin: Humboldt University at zu Berlin, 2004.

　　［10］ 骆翔宇，王昆，王凤钗. 一种Web服务组合的认知模型检测方法［J］.小型微型计算机系统，2011，32(10)：2042-2047.

　　［11］ 彭洁. 基于着色Petri网的工作流建模与实现［D］. 南昌：江西理工大学，2009.

　　［12］ 门鹏，段振华. 基于着色Petri网的BPEL建模与验证［J］.西北大学学报，2007，37(6)：986-990.