Research On Formal Description Technology Of Web Service Composition Based On Algebraic Specification

Service-oriented computing(SOC)has attracted more and more attention recently,which uses web services as fundamental elements.Combining individual services released on the Intermet into a more powerful and reliable system is the only way to achieve the true capability of SOC.Therefore,service composition and verification has become a challenge in the research field of web service.Formal semantic description of service composition can support the verification and testing of the correctness of composition.However,studies on service composition formalization mainly focus on modeling and verifying the interaction behavior among services,which lack the concern about the functional correctness of service composition.This thesis extends the existed service-oriented algebraic language and proposes an algebraic specification method to specify the abstract functions and interaction behaviors of the composition formally,which lays a theoretical foundation for the verifiability and testability of service composition.The thesis mainly includes the following three aspects:1.To specify the services composition,the service-oriented algebraic specification language SOFIA is extended to further enhance the capabilities and modularity of the language.For the first time,the complete syntax and the formal definition of the extended SOFIA language are given and the parser of SOFIA language is designed and implemented based on JavaCC.The correctness of the grammar and type of the term in the specification are checked and stored in database for later use of testing.2.Algebraic specifications for existing service-oriented systems do not describe the implementation of the composition.We proposed a service-oriented algebraic specification method,and a package facility is introduced to support this method.To specify service compositions,the specification packages for the services to be composed are imported to specify how the composite service operations invokes those operations defined in the composed services.Such a specification defines the implementation of the service composition,thus called the implementation spec.In addition to these,the composed services are also specified algebraically by defining the service operations and the required functional and behavioural properties abstractly.This forms a second specification,which is called the abstract spec.These two specs must satisfy the so-called "implements" relation defined in this paper.It is explained that,when such a relation holds,a program satisfies the implementation spec implies that it also satisfies the abstract spec.This lays a foundation for verifying and testing the correctness of a service composition description with regard to a formal specification.We designed and implemented a derivation tool to help to derive whether the "realization" relationship is established.3.Apply the service-composition-oriented algebraic method to several systems for case studies.Services to be eomposed and the composite service are specified in SOFIA,and whether the implementation of composition is correct has been prooved.Finally,the thesis analyzes the abstraction,expressibility and verifiability of the proposed method.