Realizability Analysis of Top-Down Web Service Composition Specifications

Abstract

A conversation protocol specifies the desired global behaviors of a Web service composition in a top-down fashion. Before implementing a conversation protocol, its realizability has to be determined—that is, can a bottom-up Web service composition be synthesized so that it generates exactly the same set of conversations as specified by the protocol? This chapter presents three sufficient conditions to restrict control flows of a conversation protocol for achieving realizability. The model is further extended to include data semantics of Web services into consideration. To overcome the state-space explosion problem, symbolic analysis techniques are used for improving the accuracy of analysis. The realizability analysis can effectively reduce the complexity of verifying Web services with asynchronous communication.