Web Service Analysis Tool

People

• Tevfik Bultan, email: bultan AT cs.ucsb.edu
• Xiang Fu, email: Xiang.Fu AT hofstra.edu
• Jianwen Su, email: su AT cs.ucsb.edu

General Description

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 the related 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)

1. Installation Instructions
2. Running Samples
   • Stock Analysis Service. (GA Conversation Protocol)
   • Three Realizability Analysis Examples. (Standard FSA Conversation Protocol)
   • Loan Approval Process. (Interacting BPEL4WS Web Service Composition)

Source Code Download

• Version 0.1.  of wsat_source.tar.gz (250 kb). When decompressed, the file is extracted into a directory EDU/ and a file wsat.java.
• ^New The bundled tool of WSAT and BPWS4J can be found here

Tool Documentation

• WSAT supports both bottom-up and top-down specifications of Web Services, the following documents and links illustrate the syntax of input.
  • XPath : XML query language to access and manipulate data. XPath is used both in bottom-up specification (BPEL) and top-down specification (Guarded Finite State Automata Conversation Protocol). Currently our tool supports the abreviated syntax of XPath version 1.0.
  • Bottom-up: each peer is described using a BPEL business process, and the public data/port declaration uses WSDL.
    • BPEL (Business Process Execution Language for Web Services). WSAT supports BPEL version 1.1
    • WSDL (Web Service Description Language). WSAT currently supports WSDL version 1.1
  • Top-down: the desired message exchange is specified by a single Guarded Finite State Automaton, which is called "Conversation Protocol".
    • Theoretical background: see references [WWW '03], [CIAA '03], [WWW '04]
    • GFSA.html contains the syntax rules of defining conversation protocols.
• WSAT Manual (under construction)

Publications

1. [ICWS'04] X. Fu, T. Bultan, and J. Su. Realizability of Conversation Protocols With Message Contents, 2nd International Conference on Web Services (ICWS), 2004
2. [ISSTA'04] X. Fu, T. Bultan, and J. Su. Model Checking XML Manipulating Software, International Symposium on Software Testing and Analysis (ISSTA), 2004
3. [CAV'04] X. Fu, T. Bultan, and J. Su. WSAT: A Tool for Formal Analysis of Web Services, 16th International Conference on Computer Aided Verification, July 2004 (Tool paper)
4. [SIGMOD'04] R. Hull and J. Su. Tools for Design of Composite Web Services, ACM SIGMOD International Conference on Management of Data, June 2004 (Tutorial abstract). Turorial Notes
5. [WWW'04] X. Fu, T. Bultan, and J. Su. Analysis of Interacting BPEL Web Services, 13th International World Wide Web Conference (WWW), May 2004
6. [UCSB-CS-TECH-REPORT-2004-10] Xiang Fu, Oscar H. Ibarra, Jianwen Su and Tevfik Bultan. Message Based Behavior Model of Web Services: Expressive Power
7. [REOS'03] Xiang Fu, Tevfik Bultan and Jianwen Su. A Top-Down Approach to Modeling Global Behaviors of Web Services, Workshop on Requirements Engineering and Open Systems (REOS), Montery, CA, September 2003
8. [CIAA'03] Xiang Fu, Tevfik Bultan and Jianwen Su. Conversation Protocols: A Formalism for Specificationa and Verification of Reactive Electronic Services, Proc. of 8th International Conference on Implementation and Application of Automata (CIAA'03), LNCS 2759, pp. 188 - 200, Springer, Santa Barbara, July 2003. Invited journal version (.pdf)
9. [WWW'03] Tevfik Bultan, Xiang Fu, Richard Hull, and Jianwen Su. Conversation Specification: A New Approach to Design and Analysis of E-Service Composition, Proc. of Twelfth International World Wide Web Conference (WWW2003), ACM 1-58113-680-3/03/0005, pp. 403 - 410. Budpeset, Hungary, May 2003