基于多元Pi-演算的Web服务组合描述与验证

胡 静，饶国政，冯志勇

基于多元Pi-演算的Web服务组合描述与验证

胡 静，饶国政，冯志勇

(天津大学计算机科学与技术学院，天津 300072)

验证问题是Web服务发展中亟待解决的关键问题之一，类型系统的加入以及Web服务动态的体系结构给问题的解决增添了很多难度．针对上述问题，在多元Pi-演算的基础上给出Web服务的描述模型和子类型关系定义，并对Web服务的相容性进行细化，给出Web服务可替换性定义；基于这些模型和定义，给出Web服务构造时类型正确性的判定规则和运行时可替换性的判定方法；最后用1个例子说明上述规则和方法的可行性．结果表明上述模型、定义和方法为解决动态的、类型化的Web服务验证问题提供了理论依据和基础．

多元Pi-演算；Web服务验证；Web服务可替换性

Web服务组合在面向服务的计算(serviceoriented computing，SOC)模型下，无缝地访问众多分布式服务，满足了日益复杂和精巧的业务需求．基于全局和局部两个不同视角产生的Web服务组合描述规范，使得验证问题和合成问题变得非常具有挑战性[1]．验证问题，即验证某一个编排或者编制在关键系统属性方面是否正确或者他们是否互相一致；合成问题，即决定一个编排是否可以由某个编制进行实现，如果可能的话，合成一个编制的原型．

针对第1个问题的建模和形式化验证的研究工作主要集中在使用有限状态自动机[2]、进程代数[3]、 Petri网[4]、有向图[5]等形式化方法方面．

一些验证工作将WS-BPEL和WS-CDL用形式化方法描述，并且使用已有的模型检测工具进行验证，这些工具有Uppaal[6]、Java Path Finder[7]或者是NusMVC[8]．然而这些形式化方法和验证工具并不是针对Web服务组合而设计的验证和优化方法．

还有一些验证方法是专门针对Web服务组合的特性提出的．文献[9]从全局和局部2个不同的视角提出形式化方法和基于符号模型检测的一致性检查．在文献[10]中一致性的概念是通过自动机定义的，而且仅限于2个服务之间的组合．文献[11]用Petri网的方法对Web服务组合进行形式化描述，其工作集中在检查编排中的规范在运行时是否被遵守．

Foster等建立Web服务有限状态进程(FSP)，并采用基于FSP的验证技术来对Web服务进行验证，确定了在Web服务验证中的资源约束模型[12]和验证方法，并开发了名为LTSA-WS[13]的工具．

这些方法大多是针对在Web服务组合对服务的固定绑定前提之上的．而在实际应用中，Web服务组合中各个Web子服务之间的绑定关系是松耦合的，允许人们可以随时随地根据业务流程的需要在网上动态地发现和绑定Web子服务．

Pi-演算的特性使其可以很好地描述Web服务组合这种基于交互建立的动态体系结构．当前，基于Pi-演算的Web服务组合形式化验证的工作主要是根据Pi-演算中定义的进程弱等价性质定义Web服务组合的相容性[14-15]，并通过相容性来验证Web服务组合的运行过程和功能；或者是直接利用Pi-演算的自动验证工具MWB，通过对Web服务组合弱等价性的自动验证来完成对Web服务组合的行为验证和功能验证[16]；或者基于类型化的Pi-演算对Web服务组合进行形式化建模[17]和相容性分析．

上述工作存在3方面的问题：①引入的类型系统不是强类型系统，即没有描述信道类型和值类型之间的关系，使得当Web服务组合描述中把信道作为输入/输出对象的动作时，类型系统无法进行类型相容性的判定；②定义的相容性验证的前提要求被验证的进程输入、输出动作的执行顺序和信道名称都必须相匹配，而在实际的Web服务组合应用中，有些动作是用来建立临时通信信道的，实现了Web服务组合动态的体系结构，但由于和具体的业务流程无关，其位置甚至发生的先后顺序都不固定，就使得现有的Web服务的相容性验证方法无法得到正确结果；③针对全局和局部两个不同的视角提出不同的形式化描述方法，而这些描述方法还是基于全局或者局部的，并未降低由于视角不同造成的Web服务组合描述间相容性验证问题的难度．

笔者针对验证问题进行研究，基于多元Pi-演算给出Web服务形式化描述模型的语法定义、子类型关系定义以及Web服务可替换性的定义；在以上定义的基础上给出Web服务的验证规则，包括在Web服务组合构造时的正确性验证规则和在Web服务组合运行时的可替换性验证规则，并给出相应的验证方法；最后通过第四方物流管理平台的例子说明上述规则和方法的可行性．

1 基于多元Pi-演算的Web服务描述模型

基于多元Pi-演算给出Web服务形式化描述模型的语法定义和子类型关系定义，并将Web服务的相容性进行细化，给出Web服务可替换性的定义．

1.1 Web服务形式化描述模型的语法定义

服务可以表示成四元组S=＜I，O，V，B＞．其中，S为服务的名字；I为服务的输入信道集合；O为服务的输出信道集合；V为服务的变量集合；B为服务的行为集合．对服务S的输入信道集合、输出信道集合、变量集合和行为集合的引用分别表示为IS、OS、VS和BS，对相应的具体元素的引用分别表示为[IS∶i]，[OS∶o]，[VS∶v]和[BS∶b]．用PS表示与服务S相关的命题集合，对其中某一个具体命题的引用表示为[PS∶p]．

定义1 Web服务形式化描述模型，即

其中![PS∶p]S是规则表达式!([PS∶p]S+(-[PS∶p]0))的简写形式，用来表示Web服务循环．

1.2 Web服务形式化描述模型的“信道-变量”子类型关系定义

在子类型关系定义中，定义了“信道-信道”的子类型关系和“变量-变量”的子类型关系，而在Web服务体系结构的动态构造中，存在着信道和变量的赋值，因此它们之间的子类型关系亟需定义．

定义2 “信道-变量”子类型关系Web服务形式化描述中信道和变量之间的子类型关系定义为

Web服务组合进行描述时，服务之间传递的信息包括数据和信道．接受者需要用变量来存储传递过来的信道，如果没有这几条规则，那么服务类型良好性判断规则无法判断信道和变量之间的子类型关系，而无法适应Web服务组合体系结构的动态生成．1.3 Web服务可替换性定义

在之前的研究工作中，大部分是用Web服务的相容性来说明当Web服务组合中某个Web服务无法使用时，用来替换的Web服务是否能够完成相同功能，并且和其原本环境交互良好．Web服务相容性的定义基于Pi-演算中进程的弱相似性，相容关系是对称的．Web服务相容性的定义和判断方法中只考虑了在交互过程中能完成相似的功能，没有考虑传递信息的类型兼容对相容性判断造成的影响．在实际应用中，类型不兼容往往是造成运行时错误的主要因素，为了能够定义和避免这种由类型不兼容带来的影响，就需要在原有的相容性定义中引入类型，将相容性定义进行进一步细化．

将Web服务相容性进行细化，引入对类型兼容性的判断，给出Web服务可替换性的定义，为后面在构造时和运行时进行的Web服务可替换性验证提供理论依据和基础．

定义3 Web服务可替换性T▻ 设服务S和R是弱相似的，去掉所有的内部转移之后，服务S经过n个动作α1，α2，…，αn之后变迁为终止的服务0，服务R经过m个动作α’1，α’2，…，α’m之后变迁为终止的服务0，其中m≥n，且S和R均为类型良好的服务，则ST▻R意味着服务S可以被服务R替换，必须要满足条件为

Web服务的可替换性是不对称关系，Web服务的相容性可以通过可替换性进行重新定义：Web服务S和R是相容的，当且仅当TS▻R并且TR▻S．

可替换性的定义表明：

(1) 当比较的2个动作同为输出时，如果R可以替换S，就要求R的客体类型是S的客体类型的子类型，这样才能够保证S的周围环境不会接收类型不兼容的变量；

(2) 比较的2个动作同为输入时，如果R可以替换S，就要求S的客体类型是R的客体类型的子类型，这样才能够使得R可以接收S周围环境发出的所有类型的变量，而不会产生不兼容问题．

2 基于多元Pi-演算的Web服务验证

基于多元Pi-演算的Web服务形式化描述模型不但可以描述Web服务的交互行为，而且扩充了强类型系统，这就使得在对Web服务进行验证时，需要同时考虑行为和类型的正确性和可替换性．

在Web服务的构造时，行为的正确性和类型的正确性可以分开进行验证，其中行为正确性的验证规则可以直接使用Pi-演算对进程正确性的验证规则，此处不再赘述；在Web服务的运行时，基于可替换性的定义，行为和类型无法分开进行可替换性的验证，需要给出可替换性验证的具体方法．

综上所述，本节给出Web服务构造时的类型正确性验证规则以及Web服务运行时可替换性验证方法．2.1 Web服务构造时类型正确性的验证

在Web服务的构造时，服务构造符(符号“|”、“+”和“！”)、τ动作以及命题条件并不会改变Web服务的正确性．构造时的类型正确性主要是保证一般的输入输出动作的主体和客体的类型符合如下的子类型关系．

规则1

规则2

规则指出为了保证服务的类型良好性，必须满足：对于输出行为(规则1)，其行为的客体的类型是行为主体可以输出类型的子类型，对于输入行为(规则2)，其行为的主体可以输入的类型是行为客体类型的子类型．

2.2 Web服务运行时可替换性的验证

对Web服务可替换性的定义，在Pi-演算进程间弱等价性的基础上加入了子类型判断，无法再利用Pi-演算的自动验证工具进行可替换性验证．基于对Web服务可替换性的定义，将Web服务的描述动作分为和业务流程相关以及和业务流程无关两大类，主要对和业务流程相关的动作进行可替换性验证，如有名字不匹配，则根据和业务无关的动作集合进行对应和代换．具体的可替换性验证方法描述如下：

(1) 验证前提．Web服务可替换性定义的基础是多元Pi-演算中进程的弱相似性，进程内部进行数据交换的动作全部转换成τ．也就是说，在对2个Web进行可替换性判定之前，要完成每个Web服务内部子服务间的交互操作，得到其和外部环境或其他Web服务进行交互的操作序列．

(2) 假设条件．设Web服务S和T均为去掉了内部交互动作之后的服务描述，服务S经过n个动作α1, α2,…,αn之后变迁为终止的服务0，服务T经过m个动作α1′, α2′,…,αm′ 之后变迁为终止的服务0，其中m≥n．

(3) 可替换性算法．Web服务可替换性的判定算法如下，其中输入是服务S和T的描述，输出是服务T是否可以替换服务S．

If(StaticCheck(S)&& StaticCheck(T)

{

ActionDivision(S)；

ActionDivision(T)；

While(SL!=NULL)

{

αi=LS；

αi'=LT；

if(（xi=xi′&& T3≤T4)||(&& T4≤T3)）

LS=LS.next；

else if(（xi≠xi′)||(xi≠xi′)）

{

∃aj∈Cs|obj(aj)=xi；

∃a′j∈CT|sub(a′j)=sub(aj)；

LT=LT{obj(a′j)/xi}；

CS=CS{aj}；

CT=CT{a′j}；

continue；

}

else return(Err)

}

return(Replaceable)

}

上述算法的步骤和主要方法说明如下：

(1) αi的表示形式是xi( y)或xi( y)．ΓS|-y: T3，a′j的表示形式是xi'(y')或xi'(y')．ΓT|-y':T4．

(2) 先要完成对服务S和T的构造时正确性检查，包括类型正确性和行为正确性．方法StaticCheck确保现有描述的类型完全符合Web服务的类型良好性判断准则，并且行为不存在死锁．

(3) 根据是否和业务流程相关完成对服务S和T中动作的划分，用列表的形式保存和业务流程相关的动作序列，和业务流程无关的动作用集合保存即可．方法ActionDivision对S和T中的动作进行划分，得到服务列表SL和TL，存储S和T中所有与业务流程相关的动作序列；得到集合SC和TC，存储服务S和T中构建临时通信信道的动作集合．

(4) 在进行可替换性比对时，如果当前的动作同为输入或者输出，并且信道名称相同，则只需要满足Web服务可替换性中定义的子类型关系即可；如果当前的动作同为输入或者输出，但信道名称不同，则表明在此位置之前可能有临时信道的建立，通过通信信道主体和客体的对应关系，找到在T中和S相应的信道名称，并完成对T中信道名称的替换，而后进入下一次的对比工作；如果当前的动作不同为输入或者输出，那么就说明服务T一定不能替换服务S．

3 Web服务组合验证的实例说明

以第四方物流管理平台作为实例，主要说明判断Web服务的可替换性算法中动作划分的必要性．第四方物流管理平台的体系结构如图1所示．每一个方框代表一个服务，实线为服务间固定的通信信道，虚线为动态信道，即从客户角度来看，与其交互的是一个组合服务，通信的信道是req和ack，而组合服务内部的信道reqs、sresp、pay和payr对客户来讲是不可见的．

图1 第四方物流管理平台的全局交互协作Fig.1 Global interaction of 4,PL

用BPEL4WS和WS-CDL分别对第四方物流管理平台的Web服务组合方式进行描述，采用文献[14]中描述的规范标签和Pi-演算中动作的对应关系，对具有嵌套结构的描述文档进行自顶向下的扫描分析方法，可以得到2个从不同角度对同一服务组合进行描述的Pi-演算描述方法．

从BPEL4WS文档得到的描述为

从WS-CDL得到的描述为

首先，对Web服务MS和MS′进行构造时的正确性验证．使用Pi-演算的自动验证工具MWB中的deadlock命令验证可知MS和MS′均不存在死锁，其构造时动作具有正确性；从WS-CDL和BPEL4WS文档中解析得到每个名字的变量，根据子类型关系规则进行判断，可知其构造时类型关系也具有正确性．

对Web服务MS和MS′进行运行时的可替换性验证．使用之前研究成果中对相容性验证的方法，在MWB中运行weq命令，可知2个服务不是弱等价的，从而无法得到2个服务相容的结果．这是因为2个服务在用户和银行之间建立通信信道的动作顺序不相同．即MS的

中动作的顺序不同．

用可替换性算法对这2个服务重新进行检测.在此重点描述以上2个出现问题的分支．在SM的分支中，笔者将和业务无关的动作进行划分，得到建立临时信道的动作集合为{reqs(sresp)，sresp(ask1)}，同样的在SM′的分支中得到建立临时信道的动作集合为{reqs(sresp)，sresp(cl)}．在可替换性算法比对期间，用SM动作集合中的ask1替换SM′的cl，然后再继续进行比对，可以得到服务SM可以被服务SM′替换．使用同样的方法可以得到服务SM′也可以被SM替换，由此得到服务SM和SM′是相容的．

4 结 语

在实际的Web服务组合中，除了发生由于数据类型不匹配产生的错误，由于发生交互的行为顺序不同，而有些顺序不同的动作是和业务流程无关的，其动作的位置顺序是可以发生变化的，这就使得使用传统的相容性验证方法会把很多原本可替换的服务判断为不可替换．

基于多元Pi-演算提出Web服务的描述模型以及子类型关系的判定规则，对Web服务的相容性进行细化，给出Web服务可替换性的定义；针对Web服务描述动作的主体类型和客体类型之间的关系，给出在Web服务构造时类型正确性验证规则；根据业务流的相关性将Web服务描述的动作进行划分，针对业务流程相关动作进行运行时的可替换性验证，期间，根据业务流程无关动作，进行Web服务描述名字的代换，而后在新的代换下进行可替换性验证；最后第四方物流管理平台的例子说明了上述验证方法中动作划分和代换的可行性．

［1］ Sun Jun，Liu Yang，Jin Songdong，et al. Model-based methods for linking Web service choreography and orchestration[C] //The 17th Asia Pacific Software Engineering Conference. Sydney，Australia，2010：166-175.

［2］ Fu Xiang，Bultan Tevfik，Su Jianwen，et al. Analysis of interacting BPEL web services[C] //Proceedings of the 13th International Conference on World Wide Web 2004. New York，USA：ACM Press，2004：621-630.

［3］ Liu Fangfang，Zhang Liang，Shi Yuliang，et al. Formal analysis of compatibility of Web services via CCS[C] //Proceedings of the International Conference on Next Generation Web Services Practices. Washington，USA：IEEE Computer Society Press，2005：143-148.

［4］ 钱柱中，陆桑璐，谢 立. 基于Petri网的Web服务自动组合研究[J]. 计算机学报，2006，29(7)：1057-1066.

Qian Zhuzhong，Lu Sanglu，Xie Li. Automatic composition of Petri net based Web services[J]. Chinese Journal of Computers，2006，29(7)：1057-1066(in Chinese).

［5］ Yun Yaoli，Jagadish H V. Compatibility determination in Web services[C]//Proceedings of the First International E-Services Workshop. Pittsburgh，USA，2003：7-15.

［6］ Dong J S，Liu Y. Verification of computation orchestration via timed automata[C]// ICFEM'06 Proceedings of the 8th International Conference on Formal Methods and Software Engineering．Berlin：Springer-Verlag，2006：226-245.

［7］ Pu Geguang，Shi Jianqi，Wang Zheng，et al. The Validation and verification of WSCDL[C] //14th Asia-Pacific Software Engineering Conference．Washington，USA，2007：81-88.

［8］ Kazhamiakin R，Pandya P，Marco Pistore. Representation，verification，and computation of timed properties in Web[C]//ICWS'06 Proceedings of the IEEE International Conference on Web Services．Washington，USA，2006：497-504.

［9］ Kazhamiakin R，Pistore M. Choreography conformanceanalysis：Asynchronous communications and information alignment[C]//WS-FM'06 Proceedings of the Third International Conference on Web Services and Formal Methods．Berlin：Springer-Verlag，2006：227-241.

［10］ Baldoni M，Baroglio C，Martelli A，et al. Verifying the conformance of web services to global interaction protocols：A first step[C] // EPEW'05/WS-FM'05 Proceedings of the 2nd International Workshop on Web Services and Formal Methods．Berlin：Springer-Verlag，2005：257-271.

［11］ Aalst W M P，Dramas M，Onyang C，et al. Conformance checking of service behavior[J]. ACM Transactions on Internet Technology(TOIT)，2008，8(3)：1-30.

［12］ Foster H，Emmerich W，Kramer J，et al. Model checking service compositions under resource constraints [C] //ESEC-FSE '07 Proceedings of the 6,th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on The Foundations of Software Engineering．New York，USA，2007：225-234.

［13］ Foster H，Uchitel S，Magee J，et al. LTSA-WS：A tool for model-based verification of Web service compositions and choreography[C]//ICSE'06 Proceedings of the 28th International Conference on Software Engineering． New York，USA，2006：771-774.

［14］ 胡 静，冯志勇. 基于Pi-演算的Web服务形式化描述模型[J]. 计算机应用研究，2011，28(6)：2168-2173.

Hu Jing，Feng Zhiyong. Pi-calculus based formal description model for Web services[J]. Application Research of Computers，2011，28(6)：2168-2173(in Chinese).

［15］ 辜希武，卢正鼎. Web服务相容性的形式化描述与分析[J]. 计算机工程与应用，2007，43(27)：28-33(in

Chinese). Gu Xiwu，Lu Zhengding. Formal description and analysis of Web services compatibility[J]. Computer Engineering and Applications，2007，43(27)：28-33(in Chinese).

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

Liao Jun，Tan Hao，Liu Jinde. Describing and verifying Web service using Pi-calculus[J]. Chinese Journal of Computers，2005，28(4)：635-643(in Chinese).

［17］ 辜希武，卢正鼎. 类型化的Web服务组合形式化模型[J]. 计算机科学，2008，35(1)：128-134.

Gu Xiwu，Lu Zhengding. A typed formal model for Web services composition [J]. Computer Science，2008，35(1)：128-134(in Chinese).

Polyadic Pi-Calculus Based Description and Verification for Web Service

Hu Jing，Rao Guozheng，Feng Zhiyong
(School of Computer Science and Technology，Tianjin University，Tianjin 300072，China)

Verification is one of the important issues to be addressed in the development of Web services，and type system and the dynamic architecture of Web services，add a lot more difficulty to it. This paper gives the description model of Web services and the subtype relationship defined on the basis of polyadic Pi-calculus，and defines replaceability to refine the concept of compatibility. Based on the above models and definitions，this paper addresses the rules to determining type correctness at construction time of Web services and the method of determining replaceability at run time. Finally，an example illustrates the feasibility of the above-mentioned rules and methods. All of the definitions and methods established in this paper provide a theoretical basis and foundation for solving dynamic and typed Web service verification.

polyadic Pi-calculus；Web service verification；Web services replace-ability

TP301

A

0493-2137(2013)06-0520-06

DOI 10.11784/tdxb20130609

2011-12-08；

2012-04-11.

国家自然科学基金资助项目(61003080)；教育部科技发展中心网络时代科技论文快速共享专项研究课题资助项目(2011117).

胡 静（1980——），女，讲师．

胡 静，mavis_huhu@tju.edu.cn.