Realizability of Conversation Protocols with Message Contents

A promising way to model the global behavior of a Web Service composition is to characterize the set of conversations among the participating Web Services. A conversation protocol specifies the desired global behaviors of a Web Service composition. The realizability problem is to decide whether, given a conversation protocol, a Web Service composition can be synthesized that generates exactly the same set of conversations specified by the protocol. This is a key problem in the top-down specification of the Web Service compositions. In our earlier work, we developed sufficient conditions for realizability of conversation protocols based on a model that abstracts the contents of the messages. The present paper extends our earlier work by allowing message contents to be used in the realizability analysis. We show that taking the message contents into account yields more accurate analysis. To overcome the state-space explosion caused by the message contents, we propose symbolic analysis techniques for the realizability conditions. In addition, we show that the analysis of one of the realizability conditions — the autonomy condition — can be done using an iterative refinement approach.