Takuan: A Dynamic Invariant Generation System for WS-BPEL Compositions

Web Services composition languages, such as the OASIS WS-BPEL 2.0 standard, open a vast new field for programming in the large. But they also present a challenge for traditional white-box testing techniques, due to the inclusion of specific instructions for concurrency, fault and compensation handling, dynamic service discovery and invocation, etc. Dynamic likely invariant generation has been successfully used to assist white-box testing of traditional imperative programs. We have implemented Takuan, a dynamic invariant generation system which infers likely invariants from actual execution logs of a WS-BPEL composition. We describe our experience during its development and show our first results based on the well-known loan example. These promising results point out that, with some refinements, Takuan can become an interesting aid in WS-BPEL composition white-box testing.