WSAT (Web Service Analysis Tool)
is a
formal specification, verification, and analysis tool
for web
service compositions. The tool supports multiple specification
approaches of composite web services, including BPEL4WS + WSDL specifications,
Guarded Automata (GA) based (top-down) conversation protocols, and
(bottom-up) GA service compositions. WSAT translates web service input into
Promela, the input language of model checker SPIN, and allows model checking
of web service designs without loss of (bounded and XPath based) XML data
semantics. In addition, WSAT provides several analyses techniques that can reduce complexities in the
formal verification of asynchronously communication web services.
The following are some of the
highlights of the tool: (Detailed
technical background can be found in our recent
publications)
- Real-world web service specification language such as WSDL and BPEL are
supported by the tool.
- Bounded XML data and XPath based data manipulation semantics can be
verified during model checking.
- Realizability analysis of conversation protocols allows a 3-step
specification/verification/synthesis paradigm: 1) a realizable conversation
protocol is used to specify global behaviors of a composite web service (given
its interconnection pattern), 2) desired Linear Temporal Logic (LTL)
properties are verified on the protocol, 3) peer implementations are
synthesized from the protocol via projection.
- Synchronizability analysis of bottom-up specified web service compositions
can significantly reduce the complexity and ensure the completeness of the
verification. Synchronizable web service compositions exhibit the same
set of global behaviors under both the asynchronous and synchronous
communication semantics. To model check a synchronizable web service
composition, it suffices to use the synchronous communication semantics (by
setting SPIN channel length to 0), and all verification results hold for the
usual asynchronous communication semantics.
- Realizability analysis and synchronizability analyses can be further
strenghthend to ensure freedom of deadlock and unspecified message receptions.
- Realizability analysis and synchronizability analyses work for both
standard Finite State Automata model (abstract control flow model) and
extended Guarded Automata (with data semantics) model. Various analyses
algorithms (with different levels of accuracy) are developed for the analyses
of the Guarded Automata model. (Currently skeleton analysis for GA
protocols and compositions are available.)
- The tool has a highly extensible architecture, with the use of GA as
intermediate representation. At the front end, other Web Service languages such as WSCI, WSCL,
BPML can be supported; and at the back-end side, depending on the data
and the arithmetic operations in the data manipulation, other model
checkers such as SMV, and Action Verifier can be called to efficiently
handle specific cases.
Getting Started (Tool
Demo)