Realizability of conversation protocols with message contents

A conversation protocol is a top-down specification framework which specifies desired global behaviors of a Web service composition. In our earlier work (Fu et al., 2003) we studied the problem of realizability, i.e., given a conversation protocol, can a Web service composition be synthesized to generate behaviors as specified by the protocol. Several sufficient realizability conditions were proposed by Fu et al. (2003) to ensure realizability. Conversation protocols studied by Fu et al. (2003), however, are essentially abstract control flows without data semantics. This paper extends the work by Fu et al. (2003) and achieves more accurate analysis by considering data semantics: to overcome the state-space explosion caused by the data content, we propose a symbolic analysis technique for each realizability condition. In addition, we show that the analysis of the autonomy condition can be done using an iterative refinement approach.