Research On Interface Model And Component Design In Service-Oriented Computing

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.