Analysis of BPEL Data Dependencies

BPEL is a de-facto standard language for Web service orchestration. It is a challenge to test BPEL processes automatically because of the complex features of the language. The current formal semantics proposed for BPEL can be categorized under three branches: process algebra, Petri- nets, and automata. Our goal is to automate the generation and execution of test cases for composed Web services. Model checking is an effective technique for automated test generation, and most mature model checkers such as SPIN and NuSMV use automata as the underlying formal model. Hence, we follow the automata branch. Unfortunately, the current automata based approaches omit the BPEL data dependencies. In order to address this shortcoming, we demonstrate how to model BPEL data dependencies in our proposed Web service automata.