Automatic dynamic generation of likely invariants for WS-BPEL compositions

The wide adoption of Web Services has led to the development of languages to compose them, like the WS-BPEL standard. In order to check whether the composition works as expected, one common approach is to analyze it and infer functional properties describing its behavior. Traditional approaches for inferring properties in WS-BPEL have been static: compositions are transformed into specialized analysis models based on some formalization. However, this formalization could be inexact due to theoretical limitations or differing interpretations of the standard by implementers. Dynamic invariant generation solves these problems by extracting the properties from actual executions and has been successfully used in popular languages, but not to WS-BPEL yet. In this work, we apply dynamic invariant generation to WS-BPEL, providing innovative solutions for several features that require special consideration, like highly multidimensional values in variables, an advanced type system or unstructured code. We have implemented these solutions in Takuan and evaluated its performance with several compositions of varying complexity. We present the results obtained and a comparative analysis of the efficiency and effectiveness of our solutions. Results show that the solutions are successful in reducing the cost of applying dynamic invariant generation and the number of uninteresting invariants generated.