The Consistency of Web Conversations

We describe BPELCheck, a tool for statically analyzing interactions of composite Web services implemented in BPEL. Our algorithm is compositional, and checks each process interacting with an abstraction of its peers, without constructing the product state space. Interactions between pairs of peer processes are modeled using conversation automata which encode the set of valid message exchange sequences between the two processes. A process is consistent if each possible conversation leaves its peer automata in a state labeled as consistent and the overall execution satisfies a user-specified predicate on the automata states. We have implemented BPELCheck in the Enterprise Service Pack of the NetBeans development environment. Our tool handles the major syntactic constructs of BPEL, including sequential and parallel composition, exception handling, flows, and Boolean state variables. We have used BPELCheck to check conversational consistency for a set of BPEL processes, including an industrial example.