The Consistency of Web Conversations

11 years 24 days ago
The Consistency of Web Conversations
Abstract—We describe BPELCheck, a tool for statically analyzing interactions of composite web services implemented in BPEL. Our algorithm is compositional, and checks each process ing 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 ...
Jeffrey Fischer, Rupak Majumdar, Francesco Sorrent
Added 31 May 2010
Updated 31 May 2010
Type Conference
Year 2008
Where KBSE
Authors Jeffrey Fischer, Rupak Majumdar, Francesco Sorrentino
Comments (0)