李靖 崔仲远

摘 要： 针对Web服务组合的有效性验证问题，提出了一种基于服务分组和调用轨迹的Web服务组合形式化验证方案。首先，基于服务调用顺序，利用提出的Web服务集分组（WSSG）算法将候选Web服务划分为几个子集，并结合调用轨迹编排这些子集组成WSSG图，作为系统的抽象模型；然后，推理出系统所需的预期交互规范，并利用线性时序逻辑（LTL）来描述交互规范；最后，通过检测模型是否符合交互规范来验证组合模型的可行性。实验结果表明，该方案能够有效验证Web服务组合的正确性，且避免了死锁现象。

关键词： Web服务组合验证； 建模； 调用轨迹； 线性时序逻辑

中图分类号： TN911?34； TP311 文献标识码： A 文章编号： 1004?373X（2016）05?0126?05

0 引 言

Web服务是一种基于网络的、分布式的模块化组件。由于单一Web服务功能有限，所以需要将不同的Web服务进行组合，提供更为强大的功能，满足不同用户的需求[1]。由于Web服务组合常用于跨平台、跨组织的分布式环境，服务组合在执行过程中可能会受到通信模式的变化、服务基础设施失效等问题的影响，所以有必要对Web服务组合的有效性和可靠性进行验证[2]。

目前，Web服务组合的验证方法主要包括模型检查、Petri网、Pi?演算、遗传算法、行为时序逻辑（TLA）和基于推理的交互时序逻辑等[3]。文献[4]提出一种Web服务组合的正确性验证方法，即采用软件体系结构描述语言XYZ/ADI，描述Web服务组合，其性质（规范）用CTL公式表示，最后用模型检测工具UPPAAL验证Web服务组合的正确性。文献[5]提出一种基于Petri网理论的Web服务组合建模方法，即对服务组合进行形式化建模，通过分析Web服务网的可达性和活性验证Web服务组合。文献[6]利用Pi?演算对Web服务组合建立形式化模型，定义了Pi?演算到BPEL4WS的概念映射，给出了基于Pi?演算的形式化描述。然而，这些方法都有自身的缺陷，例如：中间语言的参与、无法捕获递归组合、更多的时间和空间复杂性等。

模型检测（Model Checking，MC）是一种形式化验证方法，用状态迁移系统表示系统的行为，用时序逻辑公式描述系统的属性[7]。这样“系统是否具有所期望的属性”就转化为数学问题“状态迁移系统是否是公式的一个模型”。模型检测方法具有自动化程度高、能够提供反例路径等优势，被广泛应用于Web服务组合相关属性的验证[8]。然而随着系统规模的不断扩大，这种以穷尽搜索为基础的方法将会产生状态空间“爆炸”问题，成为验证大规模系统的瓶颈[9]。

本文采用模型检测方法，并对其存在的缺陷，提出一种新的形式化模型来推理和动态验证Web服务组合。利用提出的Web服务集分组（Web Service Set Grouping，WSSG）算法将候选Web服务划分为几个子集，并将这些子集组成Web服务集分组图（WSSG图），作为系统的抽象模型；然后，将该模型转换为交互轨迹的集合，来推理系统需要的预期交互规范，并利用线性时序逻辑（Linear Temporal Logic，LTL）[10]来描述交互规范；最后，通过检测系统模型是否符合交互规范来验证组合模型的可行性。 本文服务交互验证方案主要包括两个部分：Web服务组合系统建模和Web服务组合验证。

4 结 语

本文提出了一种Web服务组合形式化验证方法。首先，对服务组合进行建模，利用提出的Web服务集分组（WSSG）算法将候选Web服务划分为几个子集，并结合调用轨迹编排这些子集组成WSSG图，作为系统的抽象模型；然后，推理系统所需的预期交互规范，利用线性时序逻辑（LTL）来描述交互规范；最后，通过检测模型是否符合交互规范来验证组合模型的可行性。通过旅行社场景实验表明，本文方案能够有效验证Web服务组合的正确性。

在今后的工作中，将考虑失败任务的替代验证和冗余校验，来扩展本文验证方法。

参考文献

[1] 温涛，盛国军，郭权，等.基于改进粒子群算法的Web服务组合[J].计算机学报，2013，36（5）：1031?1046.

[2] 张广泉，狄浩军，石慧娟，等.基于扩展自动机的服务组合静态与动态验证方法[J].通信学报，2012，33（z1）：1?8.

[3] KLAI K， TATA S， OCHI H. Generic and specific compatibility criteria for Web service composition： formal abstraction and modular verification approach [J]. International journal of Web services research， 2012， 9（9）： 45?68.

[4] 张广泉，戎玫，朱雪阳，等.基于XYZ/ADL的Web服务组合描述与验证[J].电子学报，2011，39（3）：86?93.

[5] WANG Y Y， CHEN P. Web service composition verification of safety properties： an approach based on predicate abstraction [J]. Advanced materials research， 2013， 55（4）： 2892?2899.

[6] 胡静，饶国政，冯志勇.基于多元Pi?演算的Web服务组合描述与验证[J].天津大学学报（自然科学与工程技术版），2013，46（6）：520?525.

[7] 骆翔宇，谭征，苏开乐，等.一种基于认知模型检测的Web服务组合验证方法[J].计算机学报，2011，34（6）：1041?1061.

[8] ZAHOOR E， MUNIR K， PERRIN O， et al. A bounded model checking approach for the verification of Web services composition [J]. International journal of Web services research， 2013， 10（4）： 62?81.

[9] CHEN T W， GENG S Y. Verification of time constraints consistency on Web service composition based on ETPN [J]. Applied mechanics and materials， 2011， 60： 1094?1099.

[10] 周宁，刘慧，王红兵，等.采用动作时序逻辑的Web服务组合方法[J].计算机科学与探索，2011，5（3）：208?220.

[11] SUMATHI S， CHIPLUNKAR N N， ASHOK K A. Dynamic discovery of Web services using WSDL [J]. International journal of information technology and computer science， 2014， 6（10）： 56?62.

[12] DUMEZ C， BAKHOUYA M， GABER J， et al. Model?driven approach supporting formal verification for Web service composition protocols [J]. Journal of network and computer applications， 2013， 36（4）： 1102?1115.

[13] RAI G N， GANGADHARAN G R， PADMANABHAN V. Algebraic modeling and verification of Web service composition [J]. Procedia computer science， 2015， 52（1）： 675?679.

[14] KIL H， NAM W. Semantic Web service composition using formal verification techniques [C]// Proceedings of EL， DTA and UNESST 2012 Generation Information Technology Confe?rence. Gangneug： EL， DTA and UNESST， 2012： 72?79.

[15] BARYANNIS G， PLEXOUSAKIS D. Fluent calculus?based semantic Web service composition and verification using WSSL [J]. Lecture notes in computer science， 2013： 256?270.