Takuan is a dynamic invariant generation system for WS-BPEL. Its input are a WS-BPEL composition and a test suite (a set of test cases). And it produces in its output a set of invariants (asserts) hold before or after certain program instructions. Those invariants have different uses:
- Using invariants for documenting a composition: invariants can automatically document a composition.
- Using invariants for debugging: an invariant can show a bug in the code.
- Using invariants for verification: invariants can help you verify a composition.
- Using invariants for monitoring: invariants can be helpful to monitor a deployed (in use) composition.
- Using invariants to improve a test suite: invariants can show deficiencies in a test suite.
- Using invariants to support composition upgrading: an invariant can show a bug in an improved composition.
As you can see, these uses allow not only the external (black-box) study of a composition, but also an internal (white-box) analysis.
If you consider there is any other use or any of these uses is not rightly explained, please contact Manuel Palomo