支持Web服务组合与验证的形式化模型

摘要：针对Web服务的组合与验证问题，在范畴理论描述框架的基础上，引入进程代数描述服务组件的外部行为，为Web服务系统的架构描述建立了一种形式化的语义模型。Web服务作为范畴理论中的对象节点，服务间的交互和组合关系作为态射，从而以范畴图表的形式来描述服务网络。在形式化定义服务接口、Web服务、服务组合等概念的基础上，进一步分析讨论了服务组合和交互过程中的语义特性，给出了Web服务可替代性和服务请求可满足性的形式化定义。实例研究表明，该框架增强了Web服务架构的语义描述能力。，为基于服务模式的应用系统的理解、交互和验证提供了更加丰富的语义信息，可用于指导服务系统的模型描述和应用开发。自我评价性描述，删除

关键词：Web服务；服务组合；形式化模型；范畴理论；进程代数

中图分类号： TP311 文献标志码：A

英文摘要

Abstract：To solve the problems of Web service composition and verification， a formal model was proposed based on the framework of category theory. Process Algebra was introduced into the framework to describe the external behavior of service component， establishing a formal semantic model for the architecture of Web service system. The service network was described with category diagrams， in which Web services were used as categorical objects， and the interactive and composition relationships between services were used as morphisms. On the basis of the formal definitions of service interface， Web service and service composition， a further analysis and discussion about the semantics of service composition and interaction was undertaken. The concepts on Web service substitutability and service request satisfiability were formally defined. The application research shows that the proposed framework enhances semantic description capabilities of Web service architecture.， and provides richer semantics for the understand， interaction and validation of application system based on service mode， and thus can be used as a new guidance for the modeling and development of servicebased systems.

英文关键词

Key words：Web service； service composition； formal model； category theory； process algebra

0 引言

近年来，随着Internet网络应用模式向着云计算不断推进，服务计算在工业界和学术界都取得了长足的发展，传统的计算系统和软件系统正逐步演变为服务系统[1]。Web服务作为一种随时可被用户访问的互联网资源，可以方便地满足用户需求，是实现面向服务计算的主要技术。

通常Web服务的功能划分较细，设计粒度小，单个服务难以满足大粒度的复杂用户需求，需要将多个服务按逻辑关系进行组合[2]。另一方面，利用组件的可重用性对已的小粒度服务进行有效组合，可以很好地降低软件开发的难度，提升开发效率。服务组合是Web服务应用中的一项关键技术。

当前已有许多关于服务组合的研究[3-4]，其实施方法也相对成熟，但在Web服务组合的工程实现方面还存在许多问题：这里说有许多问题，后面至少要列3个如何准确描述Web服务的语义？如何根据服务的语义描述实现服务的自动组合？如何自动验证组合后的服务是否满足用户的需求？等等。句子不通在这些方面，距离语义Web服务的最终目标――实现服务的自动发现、调用和组合，尚有很大的差距[5]。如何准确描述Web服务的语义，如何根据服务的语义描述实现服务的自动组合，如何自动验证组合后的服务是否满足用户的需求等，在这些方面，距离语义Web服务的最终目标――实现服务的自动发现、调用和组合，尚有很大的差距[5]。能否有效地组合分布于网络中的各种服务，实现服务之间的高效集成和验证，已成为服务计算发展过程中的一个主要瓶颈[2]。

范畴理论[6]能为软件系统的层次结构提供形式化的语义描述。在前期工作[7]中，已将范畴理论用于软构件和体系结构模型之间映射关系的描述。本文进一步扩展了这种思想，在范畴理论描述框架的基础上，引入进程代数描述服务组件的外部行为，为Web服务系统的架构描述建立了一种形式化的语义模型，增强了Web服务架构的语义描述能力，为基于服务模式的应用系统的理解、交互和验证等提供了更加丰富的语义信息。该方法支持服务的自动组合及语义特性验证，可用于指导服务系统的模型描述和应用开发。

1 Web服务的形式化模型

本文中服务的形式化模型是基于范畴理论的。有关范畴理论的基础知识及定义可参考文献[6-7]，这里不再赘述。

本文通过一个目前较为流行的网上旅游服务系统[8]作为实例，贯穿全文来说明相关的概念和模型。图1描述了这个旅游服务系统的基本结构，它包含了七个服务部件：用户窗口（UserWindow）、旅游信息查询系统（Query）、网上支付系统（Payment）、地接旅行社（TravelAgency）、车辆服务（Vechile）、旅馆服务（Hotel）和导游服务（TourGuide）。

当游客使用这个组合服务时，首先调用UserWindow组件输入预期的参数（旅游线路、日期、价格范围等），UserWindow组件接收到这些数据后传递给Query组件，Query组件根据用户的要求在数据库中进行查询，并把查询结果反馈给用户。如果用户在查询结果中选择了中意的旅游产品，则系统会调用网上支付系统Payment来要求客户支付相关的费用。用户付款成功后，服务系统需要根据用户的要求来分别联系地接旅行社TravelAgency。地接旅行社收到相应的要求信息后，要分别调用车辆服务Vechile、旅馆服务Hotel、导游服务TourGuide，都收到成功的信息后，向系统返回确认信息和相应的参数。旅游服务系统再将成功预订的确认信息和相应的数据信息传递给游客。在这里，如果游客的旅行线路较长，可能是若干个地接社先后来承担相应的旅行任务，本文为简化问题的处理，假定一个地接社就可以完成客户要求的所有任务，这并不影响对问题的分析。

1.1 服务及服务接口

在基于Web服务的系统中，服务接口为服务组件提供了功能描述以及参数和返回值等信息，规定了Web服务间的控制依赖和数据依赖，是服务调用以及服务间协同合作的基础。参考文献[9-10]，给出如下的服务端口标识定义。

定义1 服务接口标识。接口标识形式化定义为一个六元组SSP=〈PN， PT， MS， OS， MOP， MOM〉。其中：

1）PN是服务接口名。

2）PT是服务接口的类型，分输入/输出两种。

3）MS是服务接口上可能出现的消息构成的集合。

4）OS是服务接口所涉及的操作组成的集合。

5）MOP： MS2Mntd是一个由映射关系构成的集合，给出了接口消息所携带的信息。其中：MntdSname×Stype×Sdspt是消息参数的集合， Sname是由参数名称组成的集合，Stype是由参数类型组成的集合，Sdspt是参数语义描述信息的集合。

6）MOM： OS2Ms为操作集合OS到消息集合MS的映射关系构成的集合，给出了操作的参数信息。

本文将进程代数（Process Algebra， PA）[11]引入到范畴理论框架中，来形式化描述服务的外部行为以及服务组合的动态语义，有关的基础知识请参考文献[7，11]。

定义2 Web服务。Web服务形式化定义为一个九元组SWS=〈NWS， IDWS， Σ， PSIN， PSOUT， DSFN， DSNF， BHWS， MBO〉。其中：

1）NWS是Web服务名。

2）IDWS是Web服务的唯一标识，用ID来判别不同的服务接口。

3）Σ=〈S， Ω〉是在代数意义上服务系统描述所使用的数据标识[7]，S是描述数据类型所使用的符号集，Ω是由S*×S所定义的函数符号集合。

4）PSIN是由服务的输入接口构成的集合。

5）PSOUT是由服务的输出接口构成的集合。

6）DSFN={〈Object，Action，Pre，Effect〉}是服务的功能特性描述信息构成的集合。Object代表服务的处理对象，Action代表实现该功能所要执行的动作，Pre是前提条件，Effect是执行效果。

7）DSNF={〈NAT， OCMP， VREF〉}是服务的非功能特性描述信息构成的集合。这里NAT代表某一非功能属性名称，VREF是指定的参考值，OCMP是用于跟VREF作比较的运算符号。

8）BHWS是用进程代数PA来形式化描述的服务外部行为。

9）MBO： { e|e∈BHWS }{op|op∈ PSIN∪PSOUT}表示行为描述与接口描述之间的映射和关联关系，阐述了行为描述中的触发动作跟接口描述中的操作间的对应关系。

进程代数具有很强的表达能力，将其引入到范畴理论框架中，可以将Web服务行为及其组合置于严格可判定推理的框架之下，从而讨论其相关性质。

定义4和定义5中的第7）项，说明对不同性质的组合结构，组合后服务的非功能属性项计算方法也不一样。例如对于服务响应时间，并行组合后的整体响应时间为子服务响应时间的最大值，而顺序组合后是各个子服务的响应时间之和。

在范畴图表上，通过余极限操作进行服务组合，组合后的服务描述为由各个子服务和服务态射组成的子范畴[7]，其中服务是节点，服务态射说明了服务之间的调用和交互。通过对组合态射的递归应用，同时配置相应的结构约束和行为约束，在范畴图表语义上，把整个Web服务系统描述为一个大的服务组合，这样就得到一个有限余完备范畴[6]。

基于上述理论和方法，图1中旅游服务系统的范畴图表如图2所示。可以这样来描述服务组合的次序：在Web端，用户窗口（UserWindow）和旅游信息查询系统（Query）先组合在一起构成旅游线路信息服务系统（TourServer），然后TourServer再与网上支付系统（Payment）组合在一起构成Web旅游服务系统（WebTravel）；在地接社面，车辆服务（Vechile）和旅馆服务（Hotel）先组合在一起提供交通住宿综合服务系统（VechileHotel），这两个服务是可以完全并行的组合。然后VechileHotel再与地接旅行社（TravelAgency）组合在一起提供旅游的地接预订服务（LocalOrder），接下来LocalOrder与导游服务（TourGuide）组合在一起构成地接旅游服务系统（LocalTravel）；最后是WebTravel与LocalTravel组合在一起提供整个网上旅游服务（TravelService）。为便于理解，在图2中添加了虚线圆圈表示服务的逐层组合，当然它们并不包含在范畴图表中。

2 形式化模型的应用―语义分析

本质上，Web服务的组合是一个由许多服务组件组成的软件系统。形式化模型可用于服务组合语义的分析和正确性验证。

在Web服务组合中，可考察、分析及检验的语义特性有很多，本文的目的并不是全部给出这些语义方面及其验证方法，而是通过对几种常见的语义特性进行分析，介绍基于范畴理论的服务形式化模型的应用。限于篇幅，本文仅对以下几种语义进行讨论。

2.1 服务接口语义

Web服务组合表现服务计算的能力与效率，反映了可组合服务之间的信息传递关系以及它们在接口上的逻辑关系[8]，因此对服务接口的语义分析非常重要。在进行语义分析之前，先给出语义包含的定义。

定义6 语义包含。给定两个语义描述集SA和SB，如果对SA里的任一元素a，满足条件：（b∈SB（（b a）∨（b=a）），则称SB语义包含SA，记为SA这里的下标s何意是对集合“包含”符号的一种特殊定义，特指语义包含关系。S SB。这里的.何意，句号？是的，是个句号。

2.3 服务请求和服务替代

当流程中的某个服务发生失效后，就需要用到服务替代策略，必须保证替换后的服务组件可与其他的原有服务能重新进行组合，组合后的服务系统保证能正常工作。这就需要验证替换前后的两个服务（或服务组合）是否满足可替代性。为了便于更好地对Web服务之间的行为进行语义分析，这里先给出语义相容和语义覆盖两个基础定义。

定义11 语义相容。令Semantic是用于语义描述的元素组成的集合，s1，s2∈Semantic， 如果存在一个语义映射关系R，有s1=是否为变量，为何是正，不用斜不是变量，是语义相容关系的指代符。R（s2）成立，则表示在关系R下，语义元素s1所描述的实例可以用s2所描述的实例来替代，称在语义关系R上s1与s2相容，记作s1 R s2。

本文后面通常用R表示一种语义匹配关系组成的集合。

定义12 语义覆盖。令Semantic是用于语义描述的元素组成的集合，R是Semantic中语义元素间的匹配关系组成的集合，S、T是Semantic的子集，即SSemantic，TSemantic，若条件（s）（s∈S （t）（t∈T∧（s R t）））成立，则称语义集合T覆盖集合S，记作S∝T。

类似地，当需要替代Web服务或服务组合时，显然可依据定义9，通过对替代前后的两个服务中以PA形式描述的行为语义进行一致性考察，进而依据定义13来完成可替代性验证。因限于篇幅，本文省略了详细的实例介绍，将在后续研究的基础上进行阐述。

3.2 对比分析

Web服务系统构建的目标是通过整合各种服务组件，建立能够实现用户特定需求的系统服务，其中候选服务的发现、组合以及特性检测都是非常关键的技术。用形式化语义对参与组合的服务、组合过程以及待检验的特性进行描述，再用相应的检验工具进行正确性验证，便于在实施阶段根据组合规范来绑定相应的服务（或服务组合），最终使整个服务系统能够协同工作，并满足用户提出的系统需求和性质。

建立在描述逻辑基础上的Web服务本体语言（Ontology Web Language for Service，OWLS）[12]，能有效表示静态领域的知识并对其进行推理，但不具备对行为或动作等具有动态特征的方面进行有效描述和处理的能力[13]，导致无法对服务过程模型进行自动分析。此外，在OWLS过程模型中，其语义主要表现在构造算符的操作上，并没有明确定义这些算符的运行方式，不能描述服务间的交互和迁移，不能形式化描述服务组合的动态语义。基于Petri网的OWLS服务操作语义[14]，随着系统规模的不断扩大，使用Petri网描述服务操作语义存在状态空间爆炸的问题。张广泉等[15]基于精化检验和模型检测方法，从软件体系结构角度，提出了一种Web服务组合的描述与验证方法。由于模型检测是对状态空间的穷尽搜索，该方法同样无法避免状态爆炸问题。

与上述方法相比，本文所建模型使用范畴理论作为基础框架，使得问题的描述和讨论与特定服务描述语言无关。该框架支持以定理证明的方式，对服务系统的相关语义特性进行分析和验证，克服了传统方法的不足。范畴理论支持图形化建模，有利于对服务组合和交互关系的理解与追踪。实例研究表明，本文提出的方法是有效的。另外，范畴理论有许多较为成熟的推理和验证工具，如Kestrel学会开发的SPECWARE系统[16]，能基于形式化的规范描述，完成相关特性的自动验证。这为本文所提方法的进一步研究和应用提供了很好的支持。

4 结语

本文提出了基于范畴理论的Web服务形式化描述框架，增强了Web服务架构的语义描述能力，为基于服务模式的应用系统的理解、交互和验证提供了更加丰富的语义信息，可用于指导服务系统的模型描述和应用开发。下一步的工作将在范畴理论支持工具的基础上，进一步完善Web服务的形式化描述，研究建立服务组合的范畴论描述与网络服务业务流程执行语言（Business Process Execution Language for Web Services，BPEL4WS）是否有中英文全称，若有，请按缩略语规范，补充中英文全称，若没有，请说明网络服务业务流程执行语言（Business Process Execution Language for Web Services，BPEL4WS）的转换规则，将该描述框架应用于服务系统实施工程中。

参考文献：

[1]DENG S， HUANG L， WU B， et al. QoS optimal automatic composition of semantic Web services [J]. Chinese Journal of Computers， 2013， 36（5）： 1015-1029.（邓水光，黄龙涛，吴斌，等.一种QoS最优的语义Web服务自动组合方法[J].计算机学报，2013，36（5）：1015-1029.）

[2]GUINARD D， TRIFA V， KAMOUSKOS S， et al. Interacting with the SOAbased Internet of things： discovery， query， selection， and ondemand provisioning of Web services [J]. IEEE Transactions on Services Computing， 2010， 3（3）： 223-235.

[3]BARTALOS P， BIELIKOVA M. Automatic dynamic Web service composition： a survey and problem formalization [J]. Computing and Informatics， 2012， 30（4）： 793-827.

[4]CHARIF Y， SABOURET N. An overview of semantic Web services composition approaches [J]. Electronic Notes in Theoretical Computer Science， 2006， 146（1）： 33-41.

[5]SHENG Q Z， MAAMAR Z， YAO L， et al. Behavior modeling and automated verification of Web services [J]. Information Sciences， 2014， 258（2）： 416-433.

[6]BARR M， WELLS C. Category theory for computing science [M]. Upper Saddle River： PrenticeHall， 1990： 23-36.

[7]HOU J. Research on formal architectural semantics and transformational consistency supporting model driven development [D]. Jinan： Shandong University， 2008.（侯金奎.支持模型驱动开发的体系结构形式化语义与转换一致性研究 [D].济南：山东大学，2008.）

[8]EasyGo Inc. Website of Tours4Fun [EB/OL]. [2015-01-09]. http：///.

[9]CHEN Z， WANG J， DONG W， et al. An interface model for serviceoriented software architecture [J]. Ruan Jian Xue Bao/Journal of Software， 2006， 17（6）： 1459-1469. （陈振邦，王戟，董威，等.面向服务软件体系结构的接口模型[J].软件学报，2006，17（6）：1459-1469.）

[10]HOU K， BAI X， LU H， et al. Web service test data generation using interface semantic contract [J]. Journal of Software， 2013， 24（9）： 2020-2041. （侯可佳，白晓颖，陆皓，等.基于接口语义契约的Web服务测试数据生成[J].软件学报，2013，24（9）：2020-2041.）

[11]BERNARDO M， CIANCARINI P， DONATIELLO L. Architecting families of software systems with process algebras[J]. ACM Transactions on Software Engineering and Methodology， 2002， 11（4）： 386-426.

[12]MARTIN D， BURSTEIN M， HOBBS J， et al. OWLS： semantic markup for Web services [EB/OL]. [2014-11-02]. http：///Submission/OWLS/.

[13]SHI Z， CHANG L. Reasoning about semantic Web services with an approach based on dynamic description logics [J]. Chinese Journal of Computers， 2008， 31（9）： 1599-1611. （史忠植，常亮. 基于动态描述逻辑的语义Web服务推理[J].计算机学报，2008，31（9）：1599-1611.）

[14]NI Y， FAN Y. Model transformation and formal verification for semantic Web services composition [J]. Advances in Engineering Software， 2010， 41（6）： 879-885.

[15]ZHANG G， RONG M， ZHU X， et al. Specification and verification of Web service composition based on XYZ/ADL[J]. Acta Electron Sincia， 2011， 39（3A）： 86-93.（张广泉，戎玫，朱雪阳，等.基于XYZ/ADL的Web服务组合描述与验证[J].电子学报，2011，39（3A）：86-93.）

[16]SRINIVAS Y V， JULLIG R. Specware： Formal support for composing software [C]// Mathematics of Program Construction， LNCS 947. Berlin： Springer， 1995： 399-422.