Research On Analysis And Verification For Asynchronous Web Service Composition

With the rapid development of network technology, because of its good reusability, loose coupling and interoperability, Service Oriented Architecture has become a kind of network software application pattern widely accepted by both industry and academic. As the main technology to implement SOA, Web service is gradually becoming the standard way to package network resources. At present, Web service is converting from single function oriented to business process oriented, which makes the service cycle prolong. Therefore, the synchronous Web service has failed to meet user’s requirement and non-blocked asynchronous Web service becomes research hotspot.A single Web service can only provide limited functions. In order to more fully utilize the shared Web services to build enterprise-class application, Web service composition becomes more important. One of the important issues in Web service composition researching area is how to describe Web service composition formally and verify its correctness. In the process of verifying Web service composition, we not only consider the function requirement of composite service but also check deadlock caused by timed conflict or data inconformity. In this latter, composite Web service is efficient and correct.In this paper, we focus on asynchronous Web service. Meanwhile considering the relative timed and data constraints, we analyze its influence on the interactions between services and make a deep research on formal verification of asynchronous Web service composition. The major works are as follows:(1) we research on Web service composition from software architecture. After the analysis and comparisons, we know that the software architecture language XYZ/ADL based on temporal logic has more advantages in describing Web service composition. Therefore, we adopt XYZ/ADL to describe the interactive behaviors of Web service composition. The relative timed and data constraints can be indicated by XYZ/RE.(2) We build the formal model of asynchronous Web service on the basis of finite automata theory. We establish Timed Asynchronous Communication Model (TACM) for Web service with timed constraints. TACM, which accords with model check UPPAAL specification, adopts message queue to simulate asynchronous communication and describes timed constraints with standard timed automata clocks. When Web service involves timed and data constraints in the meanwhile, it can be described by Asynchronous Web Service Model (AWSM).(3) We propose formal verification approaches for two kinds of asynchronous Web service composition based on TACM and AWSM respectively. Two cases are given throughout the analysis and verification process to illustrate the approaches.