基于π演算的BPEL组合服务的形式化描述及验证

夏红星

（江苏靖江教师进修学校，江苏 泰州214500）

在SOA系统中，通常根据企业的业务需求，利用BPEL技术将各个独立的Web服务进行组装[1]。如何判断组合后的服务能够满足企业的需求，如何判断组合服务不会在运行中出现问题，这是软件开发人员交付服务前必须考虑的问题。事实上，人工设计或自动构建的服务组合可能存在死锁、活锁、状态不可达等众多问题，所以必须在部署前进行严格的验证，以及时发现服务组合中存在的问题。

所谓的Web组合服务验证就是指在实际部署组合服务系统前，通过某些理论或工具检查该服务组合流程逻辑的合理性、服务间的兼容性，从而及时发现和修正存在的问题，以免日后运行过程中给企业和用户造成损失。本文的重点是验证组合服务的内部流程逻辑[2]。

当前主要是通过基于状态转换模型的Petri网理论、自动机理论和基于进程代数模型的π演算理论对Web组合服务进行验证[1]。采用Petri网或者自动机对服务组合进行描述较直观简洁，但是当业务流程复杂、牵扯到的子服务众多且服务间的交互频繁的时候，往往会引起状态空间急剧增加，因此导致验证复杂度剧增。而π演算正是表示这种复杂行为的有效方式，可以清楚表示系统的并发交互行为。π演算采用文本的进程表达式描述系统，表达能力强且形式简洁，加之π演算中的行为理论非常适合用来描述动态并发的Web服务，因此本文采用π演算理论对服务组合进行建模和验证。

1 基于π演算的BPEL服务组合建模

1.1 π演算的语法定义

π演算是由MILNER R等人在通信系统演算CCS的基础上提出来的描述和分析通信拓扑结构动态变化的计算模型。设N为无限名字集，x、y等小写字母为名字集上的名字；A、B等表示进程；P、Q等表示进程表达式，进程表达式包括以下几种形式：

0表示空进程；P+Q表示选择执行P或者Q，只执行其中一个。

(2)并发表达式：P|Q表示并发执行进程P、Q。

(3)前缀表达式 y(x).P、yx.P、 .P：

正前缀y(x).P表示在端口y上输入名字 x，然后执行进程P。

负前缀yx.P表示在端口y上输出x后，再执行进程P；

.P称为哑前缀，表示进程外部不可见的动作，执行完进程后，再执行 P。

(4)循环表达式：！P表示无穷复制进程P。

(5)限制表达式：(x)P表示进程P在通道x上的外部动作被禁止，但是可以进行在通道x上的内部通信。

(6)匹配表达式：[x=y].P表示当条件x=y成立时才执行进程P。

(7)进程标识符：A（x，y，…，z）对每个进程来说，必须有其定义 A（x，y，…，z）∷=P，其中 x，y，…，z表示进程P中的自由名。

至此，将π演算定义如下：

1.2 BPEL描述的Web组合服务的π演算建模

1.2.1 建模算法

为了利用π演算验证BPEL服务组合，首先要将Web服务的逻辑关系映射为π演算的表达式，形式化描述Web服务组合，这个过程就是建模，算法描述如下：

(1)将BPEL服务组合中的每个Web服务看作一个π演算的进程。如果该服务本身又是一个组合服务那么将其递归细分为一系列的子服务，然后将每个子服务看作一个π演算进程。

(2)服务之间的调用关系抽象成π演算进程之间的通道上的消息交互。两个相关进程之间至少有一条通道，如果两进程间有多条顺序消息，则抽象成在一条通道上传递。

(3)根据 Web组合服务业务流程图，按照下表所示的Web服务元素与π演算的元素对应关系，将业务流程图转换成π演算流图。对应关系如表1所示。

(4)根据上一步骤产生的π演算流图，写出建模表达式，将Web服务及其组合用π演算形式化描述出来。

表1 BPEL中Web服务与π演算元素对应关系

1.2.2 建模实例

下面以基于BPEL的信贷服务系统（由客户、银行信贷受理服务、客户信用评估服务、信贷审批服务组成）为例，进行组合服务的π演算建模。

信贷服务系统的流程是：首先客户向银行信贷受理部门提出贷款请求，银行收到客户的贷款请求后，询问客户的具体贷款信息（比如客户姓名、贷款数额等），客户将这些信息反馈给银行信贷部门；银行信贷部门将客户贷款信息提交给客户信用评价部门，要求对该客户的信用状况进行评价，然后信用评价部门将评价信息反馈给信贷受理部门；信贷受理部门将客户申请信息和信用评价信息汇总初审。如果初审不通过，则直接拒绝客户的借贷活动；如果初审通过，则通知客户借贷请求已受理；然后将所有信息提交给审批部门，审批部门将审批结果反馈给信贷受理部门；信贷受理部门最后将审批结果反馈给客户，通知是否可以对客户发放贷款。具体业务流程如图1所示。

根据建模算法，将业务流程图抽象出如下的π演算流图，如图2所示。

根据π演算流图，写出借贷系统服务的建模表达式如下：

设客户-Client、信贷受理服务(Client Accepting Service)-CAS、信用评估服务 Credit Evaluation Service-CES、审批服务-Approving Service-AS。

客户服务Client在X通道上与信贷受理服务通信：

设u={X,ReqLoan,AskDetails,ProvideDetails,RefuseReq,AcceptReq,InformResult}，则：

信贷受理服务CAS在Y 通道上与信用评估服务通信：

设b={X,Y,Z,ReqLoan,AskDetails,ProvideDetails,Refuse-Req,AcceptReq,InformResult,ReqEvaluation,ReplyEvaluation,ReqApprove,ReplyApprove}，则：

信用评估服务CES在通道Y上与信贷服务通信：设 c={Y,ReqEvaluation,ReplyEvaluation}，则：

CES(c)=Y(msg).[msg=ReqEvaluation]Y.CES(c)

审批服务AS在通道Z上与信贷服务通信：

设 a={Z,ReqApprove,ReplyApprove}，则：

整个信贷服务系统LoanService由信贷受理服务(Client Accepting Service)CAS、信用评估服务(Credit Evaluation Service)CES、审批服务（Approving Service）AS 组合而成。{Y、Z}属于LoanService的内部通道，作为受限名字出现，于是信贷服务系统的定义如下：

2 基于π演算的BPEL组合服务的验证

2.1 Web服务组合内部逻辑验证的内容

Web服务组合内部流程逻辑的验证主要包括流程的可达性验证、流程的正确完成性验证、流程的活锁验证、死锁验证、观察等价性验证等，本文只验证观察等价性。验证观察等价性也就是验证两个进程是否是弱互模拟的。弱互模拟的定义：如果进程P、Q的外部行为是一致的，即模拟进程和被模拟进程在外部观察者看来具备完全相同的行为能力，其中一个进程能执行的动作另一个进程也能模拟，则称进程P、Q弱互模拟。

2.2 观察等价性和死锁的验证

本文的验证除了手工推演，还借助了自动化π演算工具MWB。MWB采用基于New Jersey SML语言编译器，适用于操作和分析动态并发系统。

理论推演：在前面建模时，将Client建模为π演算进程，这样做是出于下面验证观察等价性的需要。根据π演算相关理论和参考文献[3]提出的反转证明法，要判断系统中π演算描述的Client的逆进程ReverseClient与LoanService是否观察等价，只需要判断ReverseClient与LoanService是否是弱互模拟的。

Client的逆进程为：

设u={X,ReqLoan,AskDetails,ProvideDetails,RefuseReq,AcceptReq,InformResult}，则：

在组合服务 LoanService中，Y、Z是服务内部的私有通道，在这两个通道上的动作集{ReqEvaluation,ReplyEvaluation,ReqApprove,ReplyApprove}是对外不可见的 动作。

记消除 动作后的服务组合LoanService为LoanServiceOut，则：

对比可见，ReverseClient与LoanServiceOut的外部可观察动作集完全一致，即ReverseClient与LoanServiceOut弱互模拟，所以ReverseClient与LoanServiceOut观察等价，又LoanServiceOut与LoanService观察等价，从而ReverseClient与LoanService是弱互模拟的，即观察等价性成立。

利用MWB验证工具证明：

在MWB目录下创建LoanService.ag文件，将Client、CAS、CES、AS、ReverseClient、LoanService 的进程表达式写入文件中。然后在命令行输入”weq ReverseClientLoan-Service”，运行结果提示两个进程等价，证毕。

本文简单介绍了π演算的语法定义，给出了π演算理论形式化描述BPEL服务组合的建模算法，最后结合一个银行信贷系统的服务组合实例，进行建模和观察等价性验证。π演算是进行Web服务建模验证的有效理论工具，相信利用MWB等工具对进程表达式进行自动求逆和验证是未来的研究热点。

[1]MILNER R.Communicating and mobile systems:the π-calculus[M].Cambridge University Press,1999.

[2]DENG Shui Guang.Research on automatic service composition and formal verication.Zhejiang University,2007.