The LTSA WS-Engineer plug-in is an extension to the LTSA Eclipse Plug-in
which allows service models to be described by translation of the service
process descriptions, and can be used to perform model-based engineering
including:
- Support for models of WS-BPEL, WS-CDL and WSIF Logs
- Analysis of interaction models for specified properties (e.g. trace
equivalence, deadlock, liveness etc)
- Synthesis of composition and choreography interaction processes from
behaviour models (in the form of Message Sequence Charts)
- Verification of service behaviour models (e.g. for partner obligations)
- Validation through interactive and animated models
- Trace analysis for service composition interaction logs (e.g.
BPWS4J/WSIF Logs).
I am actively looking at integrating the BPEL Designer and Model-Checker
more closely.