Rigorous Analysis of Service Composability by Embedding WS-BPEL into the BIP Component Framework

Behavioral correctness of service compositions refers to the absence of service interaction flaws, so that essential service properties like deadlock freedom are preserved and correctness properties related to safety and liveness are assured. Model checking is a widespread technique and it is based on extracting an abstract model representation of the program defining a service orchestration or choreography. During model extraction, the original structure of the service composition cannot be preserved and backwards traceability of the verification findings is not possible. We propose a rigorous analysis within the BIP component framework. Being rigorous means that the analyst is able to reason on which properties hold and why. The BIP language offers a sound execution semantics for a minimal set of primitives and constructs for modeling and composing layered components. We formally define the WS-BPEL 2.0 execution semantics and we provide a structure-preserving translation (embedding) of WS-BPEL to BIP. Structure preservation is feasible, due to the formally grounded expressiveness properties of BIP. As a proof of concept, we apply the developed embedding to a sample BPEL program and present the analysis results for a safety property. By exploiting the BIP model structure we interpret the analysis findings in terms of the service interactions stated in the BPEL source code. A significant benefit of BIP is that it applies compositional reasoning on the model structure to guarantee essential correctness properties and avoid, as much as possible, the scalability limitations of conventional model checking.