基于SPIN的BPEL4WS建模与验证研究

孙军梅，周娇蓉

(杭州师范大学 信息科学与工程学院，浙江 杭州 310036)

0 引 言

随着Web服务组合技术的广泛应用，保证Web服务组合的正确性显得尤为重要.目前验证Web服务组合正确性的方法主要有定理证明和模型检测.由于模型检测能够为系统模型提供详尽的证据，如验证系统是否能够满足某些属性，而且现在已经有一些比较成熟的模型检测工具，如SPIN[1]、SMV[2]等，所以采用模型检测技术验证Web服务组合正确性的研究为多.在采用模型检测技术验证Web服务组合方面又可分为两个方向.一个是以OWL-S描述Web服务组合作为输入进行的研究，如Anupriya Ankolekar等人[3]对基于OWL-S和SPIN进行服务流和数据流正确性与交互性的检测；另一个就是以服务流程描述语言如BPEL4WS(Business Process Execution Language for Web Services)[4]为输入进行的研究.美国加州大学[5-6]对基于BPEL4WS描述的Web服务组合验证进行研究，他们把BPEL4WS描述的服务模型先是转换为模型语言Guarded Automata，进而转换为SPIN的输入语言PROMELA进行验证.Shin NAKAJIMA等人[7]对基于服务流描述语言WSFL描述的服务组合过程转换为SPIN的输入语言PROMELA进行验证的工作进行了研究.此外,还有一些基于Pi-演算或Petri网的对于Web服务组合的验证研究，如廖军等人对基于Pi-演算和模型检测器MWB进行服务组合的推演和验证[8]，门鹏等人基于着色Petri网的BPEL建模与验证[9].文献[10] 则对Web服务的模型检测技术进行了综述.

与上述方法不同，笔者对基于SPIN的BPEL4WS表示的Web服务组合验证进行了研究，给出了BPEL4WS语法到SPIN建模语言PROMELA的映射，最后通过一个实例，演示了笔者方法的有效性.

1 BPEL4WS的形式化描述

文章给出了一个基于Promela的BPEL4WS的形式化模型，在该模型中，对BPEL4WS中用于描述一个业务流程的基本构造元素即行为进行了形式化描述.为了便于表达，在给出每个行为的BPEL4WS定义时，只列出一些主要属性和子元素，其它属性和子元素用省略号表示.

(1) invoke

invoke行为将调用一个Web服务，其定义如下：

operation=” …” inputVariable=” …”

outputVariable=” …” …>

invoke行为里的partnerLink、portType、operation指定了要调用服务的访问点，inputVariable指定了调用的输入参数，outputVariable返回调用的结果.可以把该行为建模为：调用者通过通道qname=chan( partnerLink, portType, operation )发送输入变量和一个被约束的通道名q，然后从通道q输入调用结果.用Promela进程表示为：

qname! inputVariable, q

q! outputVariable

(2) receive

receive行为将等待一个调用请求，其定义如下：

operation=” …” variable=” …” …>

receive行为里的partnerLink、portType、operation指定了调用服务的访问点，variable用于接受请求参数.可以把该行为建模为：等待请求者通过通道qname=chan( partnerLink, portType, operation )接收请求参数和一个通道名q以用于将来返回结果.用Promela进程表示为：

qname? variable, q

(3) reply

reply行为将返回一个应答，其定义如下：

operation=” …” variable=” …”>

reply行为里的partnerLink、portType、operation指定了调用服务的访问点，variable指定了返回的应答结果.可以把该行为建模为：应答者通过通道qname=chan(partnerLink, portType, operation )返回应答结果.用Promela进程表示为：

qname! variable

(4) assign

assign行为用于变量的赋值，其定义如下：

可以用Promela里一对互补的输入输出动作来模拟变量间的赋值，建立一个内部通道assign，将变量name1作为通道assign上的输出，变量name2作为通道assign上的输入.用Promela进程表示为：

assign! name1

assign? name2

也可直接表示为 name2=name1，前提条件是这两个变量至少有一个是全局变量或者是处于同一进程中的两个局部变量.

(5) switch

switch行为根据一个或多个选择条件分支，从若干个子行为中选择一个执行.其定义为：

…

+activity

switch里的条件判断有1个或多个，条件值为布尔表达式，在Promela里可以用名字比较来模拟条件表达式.BPEL4WS中的一个对应Promela中if的一个执行序列，可用Promela表示为：

if

:: (condition) -> activity

…

:: else -> activity

fi

2 Web服务组合模型的实例验证

以下以一个运算服务组合为例具体说明用Promela对Web服务组合建模以及验证的过程.

2.1 运算服务组合的描述

运算服务组合是提供组合多个单一运算服务的组合服务.这里假设单一运算服务有两个，一个为“加法运算服务”，专门处理两个数相加，名为addService；一个为“减法运算服务”，专门处理两个数相减，名为subService.现在需要将这两个服务组合起来，即需要创建一个新的服务，称为“运算服务组合”，命名为caculatorService，它有一个运算类型的参数，当运算类型为“加法”时，调用加法服务；当运算类型为“减法”时，调用减法服务，并将调用结果返回.

2.2 运算服务组合的BPEL4WS模型

图1是使用BPEL4WS编辑工具Oracle BPEL4WS Process Manager建立的运算服务组合模型，此模型的起点是receive行为，接收客户输入的运算类型.接着的switch行为，通过两个case条件来判断所要执行的分支；若接收的运算类型是“add”，将执行第一个分支；每个case语句中又有3个子行为，第一个行为是assign，此行为是将接收到的消息赋值给加法服务的输入变量request_add，第二个是invoke行为，通过partnerLink(合作伙伴链接)调用加法服务，在调用参数中给出outputVariable=”response_add”，所以加法服务将最终返回的结果保存在response_add中；第三个行为是assign，它是将加法服务返回的结果赋值给运算服务的响应变量outputVariable；此变量值将在模型终点reply行为中反馈给客户.同理，若接收到的运算类型为“sub”，将执行第二个分支，若运算类型不是“add”或“sub”，将执行第三个分支；执行完分支活动后，亦会执行reply行为.

用BPEL4WS描述的运算服务组合源代码片段如下：

图1 运算服务组合的BPEL4WS模型

图2 Web服务组合的状态转换图

…

variable=”inputVariable”/>

inputVariable=”request_add”

outputVariable=”response_add”/>

2.3 运算服务组合的Promela模型

将上面建立的服务组合的BPEL4WS模型转化为Promela模型，用状态转换图描述的Web服务组合的业务流程如图2.

在该文验证的模型中，将初始状态设为s0，用以表示执行receive行为时的状态；将调用加法服务设为s1状态；调用减法服务设为s2状态；s3表示运算符号既不为add也不为sub时的状态，此时结束判断，执行reply行为，即s3为结束状态.用Promela描述caculatorService的源代码片段如下：

/* 程序中用到的变量都为mtype(枚举)型变量 */

proctype caculatorService()

{ ch_type? input, ch_ack ->

/* 相当于BPEL4WS的receive行为 */

end: if /* 相当于BPEL4WS的switch/case行为 */

:: (input == add & state!= s3) ->

ch_add! input, ch_addresp;

/* 相当于BPEL4WS的invoke行为 */

state=s1;

ch_addresp? output

:: (input == sub & state!= s3) -> …

/* 运算类型为sub时的行为与add时相似，所以此代码段用省略号表示 */

:: else -> output=othercaculation; state=s3

fi; …

}

proctype addService()

{ /* 加法服务的内部进程 */

end: atomic{ch_add? add_request, ch_inadd;

add_response=addcaculation;

/* 相当于BPEL4WS的assign行为 */

ch_inadd! add_response;}

/* 相当于BPEL4WS的reply行为 */

}

proctype subService(){ … }

init{/* 初始化通道、变量以及需运行的进程等 */}

2.4 基于SPIN的Web服务组合验证

文章使用SPIN的图形界面工具XSPIN[1]对上面建立的运算服务组合模型的安全性、活性和有界性3种属性进行了验证分析.

性质1安全性(Safety)，即坏的事情永远都不会发生，比如死锁之类导致系统不稳定的危险事情.

在Formula中输入：! []( (p ->! q) || (k ->! t) )

点击Run Verification按钮，结果如图3所示.图中“Verification Result: not valid”且“error: 1”，表明此公式不成立；按照SPIN的建议运行Guided仿真，观察Message Sequence Chart窗口可知模型中存在死循环，从而说明此模型存在不安全性.这是预先设计的一个注入错误，被检查出来了.

性质2活性(Liveness)，即在一个系统中好的事情最终会发生，比如请求响应.在Formula中输入：

[] ( (p -> q) || (t -> q) || (r -> q))

其中，p, t, r, q的宏定义显示在图4的Symbol Definitions编辑框中.此公式的含义是“s0到s1或s2或s3的路径或者s1到s1或s2或s3的路径或者s2到s1或s2或s3的路径总会发生”，运行公式得到如图4的验证结果.模型满足活性.

性质3有界性(Boundedness)，即任何状态都能到达结束状态.如该模型中，状态s0, s1, s2都能到达结束状态s3.图5给出了此验证的结果.从图中“Verification Result:valid”可以看到此性质成立.

图4 活性验证结果

图5 有界性验证结果

3 结束语

文章通过建立了BPEL4WS与模型检测工具SPIN输入语言Promela之间的映射关系，将用BPEL4WS描述的Web服务组合模型转化为用Promela描述的形式化模型，通过SPIN进行模型检测，验证Web服务组合模型的正确性，最后，通过一个案例给出了笔者的有效性.

今后还需在以下方面进行更深入的研究：同时考虑服务组合的数据流和控制流，分析复杂的服务组合任务；处理Web服务组合中的时间因素和事务等问题.

[1] Holzmann G J. The spin model checker: primer and reference manual[M]. Baston: Addison Wesley,2003.

[2] Mcmillan K L. The SMV system for SMV version 2.5.4[CP].http://www.cs.cmu.edu/～modelcheck/smv/smvmanual.ps,October,2006.

[3] Ankolekar A, Paolucci M, Sycara K. Spinning the OWL-S process model-towards the verification of the OWL-S process models[C]//In: Semantic Web Services: Preparing to Meet the World of Business Applications Workshop at ISWC, Hiroshima:2004.

[4] Andrew Tony. Business Process Execution Language for Web Services Version 1.1.[CP].W3C Web Site, May 2003：1-136.

[5] Fu Xiang, Bultan T, Su Jianwen. WSAT: a tool for formal analysis of web services[J]. Lecture Notes in Computer Science,2004,3114:394-395.

[6] Fu Xiang, Bultan T, Su Jianwen. Model checking interactions of composite Web services[R]. Tech Report 2004-05, Computer Science Department, University of California at Santa Barbara, California:2004.

[7] Nakajima S. Model-checking verification for reliable web service[C]. In: Proc. OOPSLA’02 Workshop on Object-Oriented Web Services, Washington:2002.

[8] 廖军，谭浩，刘锦德.基于Pi-演算的Web服务组合的描述和验证[J].计算机学报，2005,28(4):635-643.

[9] 门鹏，段振华.基于着色Petri网的BPEL建模与验证[J].西北大学学报:自然科学版，2007,37(6):986-990.

[10] 刘如娟，戴桂兰，胡长军，等.Web服务的模型检测技术探讨[J].小型微型计算机系统，2007,28(11):1921-1927.