【作者】 胡静；

【导师】 冯志勇；

【作者基本信息】 天津大学 ， 计算机应用技术， 2013， 博士

【摘要】 Web服务组合使得开发者可以基于面向服务的计算无缝地访问众多分布式服务，组合在一起解决复杂问题。大多数Web服务是独立开发并运行在异构平台上的，为了能够实现它们之间的服务组合，需要能够兼容其异构性的服务组合描述方法以及对组合后的服务进行验证或测试的方法。本文在总结以前的研究结果的基础上，以Pi-演算为基础，建立了Web服务形式化描述模型PiFM4WS，对Web服务以及Web服务组合的主要行为进行描述，为Web服务组合的动态体系结构提供统一的描述方法；将基于不同视角的Web服务组合描述规范的主要行为映射到PiFM4WS中，说明经过映射之后的两类描述规范具有等价性；将类型系统加入PiFM4WS模型中，细化了Web服务的相容性，提出可替换性的概念和验证方法；在PiFM4WS模型中对服务网络进行描述，为实现Web服务组合的自动化提供理论基础。本文所取得的主要研究成果如下：(1)建立Web服务形式化描述模型PiFM4WS：给出Web服务外部和内部行为的描述，即PiFM4WS的语法结构定义；给出Web服务经由交互发生组合的行为，即PiFM4WS的同构规则和操作语义。(2)为两类基于不同视角的描述规范的主要行为提供映射规则：为BPEL4WS规范以及WS-CDL规范的概念和各类行为提供PiFM4WS的描述方法，从语法定义和操作语义的角度说明两类不同规范的等价性，并指出PiFM4WS提供的对动态体系结构的描述方法是现有描述规范无法实现的。(3)基于类型化PiFM4WS的Web服务组合验证：将类型系统加入PiFM4WS中，根据子类型的关系细化Web服务的相容性，给出Web服务的可替换性的定义；根据信道是否和业务流程相关进行分类，结合Pi-演算中的代换算法，提出在动态体系结构下的Web服务可替换性的验证方法。(4)对服务网络进行形式化描述，为实现Web服务自动组合提供理论基础：将抽象服务和具体服务之间的通信信道进行结构的抽象和描述，为服务关系的形式化描述建立理论基础。综上所述，本文提出的形式化描述模型PiFM4WS、类型化的PiFM4WS以及服务网络的形式化描述，为Web服务组合提供了统一的形式化描述和验证框架，为实现Web服务的自动组合和验证提供了理论基础。更多还原

【Abstract】 Web service composition allows developers to compose numerousservices to solve complex problem based on service-oriented distributedcomputing. Most Web services are developed independently and runningon heterogeneous platforms, in order to achieve the combination ofservices between them, service composition description method andverification(testing) method are need to compatible with heterogeneous.This paper summarizes the results of previous study, establish the formaldescription model PiFM4WS of Web services based on Pi-calculus. TheWeb service and the main acts of Web service composition are describedin the model mentioned above, and a unified description method isproposed for dynamic Web service composition architecture. Differentperspectives based Web service composition description specificationsare mapped to PiFM4WS main acts, and the equivalence betweendifferent descriptions after mapping is proofed. The PiFM4WS model hastype system to refine Web services compatibility, and support the conceptof replaceability and verification methods. The PiFM4WS model is usedto describe the service network, and provide theoretical basis of the Webservice automation composition. The main research results obtained areas follows:(1) Establish formal description model PiFM4WS of Web services. ThePiFM4WS syntax structure definition provides description of external andinternal behavior of Web services. The PiFM4WS isomorphic rules andoperational semantics provide the interactions behaviors occur throughWeb service combination.(2) Provides mapping rules for the description of main behavioral of twodifferent perspectives: The description methods of PiFM4WS areprovided for the concepts and acts of BPEL4WS specification andWS-CDL specification. The equivalence of different specifications isproofed from the perspective of syntax and operational semantics. Thedynamic architecture description method provided in PiFM4WS, can notbe achieved in other existing models.(3) Provides Web services composition validation based on typed model PiFM4WS. The type system is added to PiFM4WS, and base on it,replaceability definition is proposed according to the relationship betweensubtypes and refines Web service compatibility. Replaceabilityverification method under the dynamic architecture of Web services isproposed according to the channel classification of process-related andcombining Pi-calculus substitution algorithm.(4) Formal description of the service network provides a theoretical basisof automatic Web service composition. The communication channelstructure between abstract services and concrete services is abstracted anddescribed, which establish theoretical foundation of the formaldescription of service relationship.In summary, this paper presents the formal description model PiFM4WS,the typed PiFM4WS and formal description of service network provide aunified formal description and verification framework, and providetheoretical basis for Web services automatic composition.更多还原