死路径消除语义下的BPEL过程建模与分析*

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

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

死路径消除语义下的BPEL过程建模与分析*

陈 莹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网

0 引言

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.1 BPEL简介与死路径消除

BPEL是一种使用XML(标准通用标记语言下的一个子集)编写的服务组合编制语言，用于自动化业务流程的形式规约语言，可以协调多个服务的执行。由于业务流程的需要，BPEL提供了基本活动与结构化活动两种不同的活动类型[8]

[9][10]。如果这个连接条件是真，则活动可以被执行，反之如果连接条件为假，则该活动不能执行并且所有通过它的均被置为假。这样的状态将一直向下传递直到遇到某个活动的变迁条件为真，此时目标活动才可以执行，这种技术称之为死路径消除。

1.2 CPN简介

着色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(expr)表示表达式expr中的变量集合；

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]。

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

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

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

其中定义3个颜色集：

colsetE=withe;colsetL=bool;

colsetACTIVE=productL×E;

9个变量：

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

funOK(l1：L) = (l1 =true)；

funSkip(l1：L) = (l1 =false)。

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

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

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

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

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

在云峰石刻的科学考察完成后，赖非等又对山东境内的秦汉刻石进行调查和捶拓。他的视野不仅在于简牍帛书和《礼器》《曹全》等汉碑，更涉及到了山东境内出土的所有汉代砖瓦、陶器、画像等等。1986年秋，赖非先生开始对山东全境的北朝摩崖刻经进行调查、测绘、记录和捶拓，历时数年。上世纪90年代，他又考察山东境内的汉画石像、历代墓志、古代玺印……山东境内的石刻分布及现状，他了如指掌，哪个字有痕，哪个字有损，哪个字在假版上错了哪一笔，没人比他更清楚。可以说，他是山东石刻研究方面当之无愧的第一人。

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

图1 单连接转换示意图

图2 双连接转换示意图

图3 两个后继link转换示意图

3 案例分析

3.1 案例描述

在本节中，采用了WS-BPEL 2.0-Primer[1]的例子来评估此方法。在图5的示例中，四个活动是并发执行的。活动开始时，四个活动同时开始执行。由于的变迁条件是完全相反的(大于或等于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语义)，提出了一种新的分析BPEL过程路径可行性方法，主要贡献分为两个方面。第一，一个新型的BPEL控制流图，即一个控制流图能抽象出WS-BPEL程序的执行过程并考虑了死路径消除语义。第二，应用CPN-Tools工具，将复杂的BPEL控制流图转换为较简单明了的流图，并运用CPN中状态空间分析工具对其进行有界性、活性等分析，从而验证了方法的可行性。

图4 包含谓词活动的转换示意图

图5 一个典型的程序

图6 CPN-Tools 状态空间报告

[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.

Modeling and analyzing BPEL processes under dead path elimination semantics

Chen Ying1, Xing Jianchun1, Wang Hongda1，Yang Qiliang1,2

(1. College of Defense Engineering, PLA University of Science and Technology, Nanjing 210007,China;2. State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing 210093, China)

Aiming at the incompleteness of BPEL processes modeling and analysis under dead path elimination semantic, this paper proposes a new BPEL process modeling and analysis method. Firstly, this method puts forward a set of rules, realizing the transformation from BPEL under death path elimination semantic to ordinary if-then-else form. Then, this method establishes the formal model of BPEL process using Colored Petri Net (CPN). Finally, the automatic analysis and verification of BPEL process model is accomplished with CPN-Tools. Case study shows that the method has practicability and feasibility, and it may help software engineers to test, debug, and maintain the BPEL process better.

Web-services; BPEL program dependence graph; dead path elimination semantics; Colored Petri Net(CPN)

江苏省自然科学基金项目(BK20151451)

TP311.5

A

10.19358/j.issn.1674- 7720.2017.06.008

陈莹，邢建春，王洪达，等. 死路径消除语义下的BPEL过程建模与分析[J].微型机与应用，2017,36(6)：22-25.

2016-10-19)

陈莹(1991-)，通信作者，女,硕士研究生，主要研究方向：任务关键系统的建模与分析。E-mail：chenying910814@163.com。

邢建春(1964-)，男，教授，博士生导师，主要研究方向：国防工程智能化、智能控制。

王洪达(1987-)，男，博士研究生，主要研究方向：服务计算、工作流测试。