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 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. In our earlier work several sufficient realizability conditions were proposed to ensure realizability. Conversation protocols studied in our earlier work, however, are essentially abstract control flows without data semantics.This paper extends our earlier work and achieves more accurate analysis by considering data semantics. To overcome the huge state space, a symbolic analysis technique is proposed for each realizability condition. In addition, the analysis of the autonomy condition can be guided by error-traces produced in previous analysis cycles.