Automatic Protocol Conformance Checking of Recursive and Parallel BPEL Systems

Today model checking of Web Services formulated in BPEL is often reduced by transforming BPEL-processes to Petri nets. These can be model checked using traditional approaches. If recursion is present in the BPEL model this approach hides some possible violations of the wished behaviour. We present an approach which allows the Web Service developer to formulate more properties of the required usage of the Web Service and provide a tool that checks whether these requirements are satisfied in a Web Service based system. We use finite state machines to specify permitted sequences of receivable interactions and call them service protocols. In this paper we will show that it is possible to use BPEL representations and service protocols to check if a sequence of receivable interactions that violates a service protocol can occur. We achieve this result by translating BPEL to Process Algebra Nets (introduced by Mayr ) and applying the approach of Mayr for model checking Process Algebra Nets. Our approach computes counterexamples even for recursive and parallel programs including synchronization.