Advanced verification of distributed WS-BPEL business processes incorporating CSSA-based data flow analysis

The business process execution language for web services (WS-BPEL) provides a technology to aggregate encapsulated functionalities for defining high-value web services. For a distributed application in a B2B interaction, the partners simply need to expose their provided functionality as BPEL processes and compose them. Verifying such distributed web service based systems has been a huge topic in the research community lately. However, in most of the work on analysing properties of interacting web services, especially when backed by stateful implementations like WS-BPEL, the data flow present in the implementation is widely neglected and the analysis focuses on control flow only. This might lead to false-positive analysis results when searching for design weaknesses and errors of a given BPEL process. In this paper, we present a method to extract data flow information by constructing a CSSA representation and detecting data dependencies that effect communication behaviour. Those discovered dependencies are used to construct a more precise formal model of the given BPEL process and hence to improve the quality of analysis results. Copyright © 2009, Inderscience Publishers.