Formal Analysis And Verification Of Web Service Compositions With Timing Constraints

With the rapid development of Web technology and the commercial application, Service-Oriented Computing(SOC) and Service-Oriented Architecture(SOA) has become the focus of People’s attention. As both of them appear, SOC and SOA solve the integration and reuse of software problems effectively in distributed and heterogeneous environment. At present, the mature chnology of Web service increasingly provides the best technical support for SOC and SOA.Web service is a software component which is based on network, and it has the characteristics of loose coupling and strong independence. Service is the basic Interactive unit of Web system. As individual Web service has its limitations, the technology of web service composition has become one of the main methods to construct the electronic commerce application. However, how to ensure that the compositions of the Web service can guarantee the quality of software in the complex environment and meet people’s expectations? Especially the limited service behavior must satisfy the condition given timing Constraints. The formal technology provides an important method to ensure the quality of software.In order to adapt to the fast-changing business environment, People puts forward the requirements of real-time for commercial applications at present. In this paper, we present a formal method for analyzing and verifying time-related properties of web service compositions. We extend web service interface with timing requirements, then introduce formalism, called Timed Behavior Automata, to capture timed behavior of web services, and verify the behavior properties of composite web services by using model-checking techniques. The case study in a model checker UPPAAL shows that our method is feasible and effective. The technology of researching service modeling and verification can guarantee the Reliability of service combination.