【作者】 陈振邦；

【导师】 齐治昌； 王戟；

【作者基本信息】 国防科学技术大学 ， 计算机科学与技术， 2009， 博士

【摘要】 面向服务计算(Service-Oriented Computing,SOC)是一种新的计算范型,SOC在流程描述、数据管理以及分布式计算中间件技术的基础上,提出以服务作为构建软件的基本单元。SOC希望通过统一的技术规范,来达到网络资源的充分利用和共享,从而提高IT企业应对需求的能力和工作效率。服务接口是SOC中服务使用者关于一个服务所能够得到的唯一信息,准确而且充分的服务接口描述是保证SOC中服务查找、服务组合等关键操作质量的重要因素。因此,如何保证接口描述的准确性,如何在服务接口描述中包含多方面的服务信息成为SOC中的关键问题。形式化方法基于严格的数学理论来提供系统的描述和分析方法,不仅能够消除系统建模过程中的不准确或歧义性,而且还能通过形式化验证来保证系统的正确性,提高系统的质量。本文希望通过研究形式化的服务接口模型及验证方法,来保证服务接口的准确性。事务是SOC中保证系统正确性和一致性非常重要的手段,SOC中的事务往往执行时间较长,需要与不同的服务提供组织协商完成,与传统事务相比,SOC中的事务对原子性和隔离性的要求相对松弛,因此SOC中一般使用长事务模型来完成具备事务要求的任务。本文针对具备长事务特征服务的接口描述,在Beyer等人提出的Web服务接口理论的基础上,提出了支持长事务行为特征描述的多层接口模型,能够分别在特征、会话和协议三个层次描述支持后向恢复长事务机制的服务在接口层面的动作引发关系。在每层接口模型的基础上,给出了基于接口的服务相容性和可替换性的检查方法。此外,为了保证服务接口的正确性,分别在三个层次给出了服务接口关键性质的规约方法和相应的验证方法。为了支持日益复杂的业务逻辑,出现了更加灵活的长事务模型,并且在目前主流的服务编制语言中都得到了体现。针对目前长事务模型中的前向恢复、事务嵌套以及可订制错误处理这些特征,本文提出了扩展协议接口来描述具备这些特征的服务接口。基于时序逻辑,给出了一般化的协议接口关键性质的规约方法,通过扩展协议接口的操作语义,采用模型检验这种形式化技术来验证扩展协议接口是否满足协议规约。为了应用扩展协议接口及验证方法,本文针对使用Web服务业务流程执行语言(BPEL)实现的服务,给出了从BPEL程序中提取扩展协议接口的方法,并使用验证方法对提取的扩展协议接口进行验证。在扩展协议接口、提取方法以及验证方法基础上,给出了它们在BPEL程序基本开发过程中的应用方式,从而可以在开发过程中验证BPEL程序,提高使用BPEL实现服务的质量。服务构件作为提供服务的计算实体,是SOC中服务提供方在服务开发过程中需要构建的主要单元。如何在开发过程中设计服务构件并保证服务构件的可靠性是提高服务质量、保证面向服务系统正确性的关键问题。与服务接口类似,本文希望通过研究形式化的服务构件建模技术以及精化方法,并在目前主流的模型驱动以及形式化验证技术基础上,寻求严格的服务构件设计方法,来提高服务构件的可靠性。本文在何积丰等人提出的构件以及对象精化理论的基础上,针对目前SOC中服务的异常行为,提出了支持异常信息描述的接口契约模型,可以支持服务接口的功能规约、服务使用方式以及异常信息多个方面的描述,并给出了不同方面行为的一致性条件,以及接口契约的数据精化方法。针对服务构件实现层面的事务特征,提出了支持补偿恢复机制的服务构件实现模型,并给出了服务构件相容性的定义。针对具备事务特征的应用,提出了支持后向恢复长事务描述的进程构件模型,用于服务构件之间的复杂组合。服务构件理论为服务构件的设计提供了理论基础,支持从接口契约到构件层面的精化,为进一步的应用形式化验证技术提供了前提。在服务构件理论的基础上,本文研究了严格的服务构件设计方法,受关注点分离(Separation of Concerns)设计思想启发,在现有模型驱动、面向对象以及面向构件理论和技术的基础上,提出了迭代以及增量式的模型驱动的服务构件设计方法,其中包括需求建模、功能设计、逻辑构件设计以及详细设计四个阶段,在每个阶段使用服务构件理论中提供的建模元素对服务构件进行建模,基于精化理论给出了服务构件设计过程中的精化方法,同时在不同的阶段使用相应的形式化验证技术保证系统模型的正确性和一致性,从而提高了服务构件的可靠性。本文最后设计并实现了接口模型的检查工具,可以对文本格式的多层接口描述进行检查和验证,同时把扩展协议接口的验证嵌入到开源的BPEL设计工具中,可以在BPEL设计过程中对其进行验证。此外,本文还设计并实现了服务构件设计工具原型,支持服务构件设计过程中的图形建模、静态和动态一致性检查、基于文本模型的自动精化等主要设计活动。更多还原

【Abstract】 Service-Oriented Computing (SOC) is a new computing paradigm, which isevolved from the techniques of process description, data management and distrib-uted computing middleware. In SOC, service is the basic unit for building software.Through unified technical specifications, SOC hopes to maximally utilize and sharethe network accessible resources.A service interface is the only information that the users of a service in SOCcan get about the service. Accuracy and su?ciency of the information in serviceinterfaces are very important to the key operations in SOC such as service discoveryand service composition. How to ensure the accuracy of an interface and incorpo-rate more information in it are critical issues in SOC. Formal Methods provide themethods of system specification and analysis based on the rigorous mathematicaltheories. By using the theories and techniques in Formal Methods, we can not onlyeliminate the inaccuracy and ambiguity in the system modeling process, but alsoensure the correctness of a system by formal verification to improve the system qual-ity. This thesis tends to ensure the accuracy of service interfaces by studying formalservice interface models and their verification methods.Transaction is a very important method to ensure the correctness and consis-tency of a system in SOC. The transactions in SOC usually last for a long time, andneed to negotiate with di?erent organizations that provide services. The require-ments of atomicity and isolation in the transactions in SOC are relaxed comparedto those of the traditional transaction. Long Running Transaction (LRT) is oftenused in SOC to accomplish the tasks with transaction requirements. Based on theexisting Web Service interface theory by Beyer et al., we propose a multi-level inter-face model for describing the interfaces of services having LRT features. The actioncausality relation of the interface representing a service, in which there are LRTs us-ing backward recovery, can be specified by using the interface model on three levels,i.e., signature, conversation and protocol. The methods for checking compatibilityand substitutivity relations of services based on interfaces are proposed with respectto our interface model. In addition, we present the specification and verification methods for critical properties on each interface level to ensure the correctness ofservice interfaces.To cope with the increasing complexity of business logic, some more ?exibleLRT models appear, and many are supported by the current de factor service or-chestration languages. A formalism, called extended protocol interface, is proposedto support describing the interfaces of services that have LRT features of forward re-covery, nested transaction and user-defined fault handing. The general specificationmethod for critical properties of protocol interface is presented based on temporallogic. Through the operational semantics of the extended protocol interface, we canverify the satisfaction of an extended protocol interface to a protocol specification byusing model checking technique. To apply the extended protocol interface and theverification method to the services implemented with Web Service Business ProcessExecution Language (BPEL), this thesis presents a method for extracting an ex-tended protocol interface from a BPEL program, and uses the verification methodto verify the extracted extended protocol interface. Based on the interface model,the extraction method and the verification method, we give their usages in the basicBPEL development process for verifying BPEL program to improve the quality ofservices implemented with BPEL.As the computing entity providing services, service component is the main unitto build in the service development process for the service providers in SOC. How todesign service components and ensure their correctness are critical issues to improvethe service quality and ensure the correctness of the system in SOC. Similar tothe service interface, this thesis tries to study the formal modeling and refinementtechniques of service component, and find the rigorous design method for servicecomponent based on the current model driven and formal verification techniques toimprove the system reliability.Based the refinement theory for component and object systems by He Jifenget al., we propose an interface contract model supporting the description of exceptioninformation with respect to the exception behavior in SOC. The interface contractmodel can contain the interface information of function specification, service invo-cation protocols and exceptions. In addition, the consistency conditions betweendi?erent aspects and the data refinement method of an interface contract are given. To support the transaction feature in the implementation of service component, wepropose a service component implementation model supporting compensation basedrecovery mechanism, and the compatibility between service components is defined.Considering the application with transaction features, we present a process compo-nent model supporting LRT using backward recovery for the complex compositionof service components. The theory of service component provides a theoretical basefor the design of service component. The refinement from service interface contractto service component is supported, and the formal service component models givethe promise for the application of formal verification techniques.By using the service component theory, this thesis studies the rigorous designmethod for service component. Aspired by the ideas of“Separation of Concerns”, wepropose an iterative and incremental model driven service component design methodbased on the current model driven, object-oriented and component-oriented theoriesand techniques. The design method contains four stages, i.e., requirement modeling,function design, logic component design and detailed design, and the modeling ele-ments in the service component theory are used in each of these stages. To improvethe service component reliability, the designer can not only use the refinement the-ory based refinement method in the design process, but also the formal verificationtechniques in the appropriate stages to ensure the correctness and consistency of thesystem models.We design and implement an interface checking tool, which can check and verifythe textual interface models, and the verification tool for the extended protocol in-terface is integrated into an open source BPEL design tool to verify BPEL programsduring the design process. In addition, we design and implement a prototype of thetool for service component design, which supports the main design activities in thedesign process such as graphical modeling, static and dynamic consistency checkingand textual model-based automatic refinement.更多还原