The Consistency of Web Conversations

We describe BPELCheck, a tool for statically analyzing interactions of composite web services implemented in BPEL. Our algorithm is composi-tional, 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 au-tomata 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 syn-tactic 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 pro-cesses, including an industrial example.