WSFM - Web Services Formal Methods

Service based architectures to cope with the increasing need for an interoperability framework between applications are currently state of the art. In particular, the advent of XML schema based interface standards like Web Services are investigated broadly from standardization organisations and vendors on a global scale. That led and will further lead to a large number of standards considered (e.g. basic Web Service specifications like SOAP, WSDL and UDDI as well as advanced Web Service specifications like WS-Federation, WS-ReliableMessaging, WS-Security, WS-Transaction or even WS-Application specification like BPEL4WS).

It is obvious that the need to proove the correctness of the design of these protocols is emerging, since most of the advanced and application specific WS protocols are not yet implemented, but will be in the near future. In order to avoid implementing design flaws a rigorous proof of important properties has to be applied at the level of design abstractions. Since most of the currently used FDT's are focusing either on implementation abstractions or on interaction abstractions (e.g. Hoare style abstractions), a specific need to support design abstractions is evident.

This observation has lead to the project, which investigates the use of the most advanced and tool supported specification approach called Temporal Logic of Actions (TLA+) (Leslie Lamport: Specifying Systems, Addison-Wesley, 2003 and http://research.microsoft.com/users/lamport/tla/tla.html) developed by Leslie Lamport for proving safety and liveness properties of WS design specifications. As a starting point the WS Atomic Transaction specification was chosen.

• 4-10.039V
  James E. Johnson, David E. Langworthy, Leslie Lamport, Friedrich H. Vogt: Formal Specification of a Web Services Protocol. In: Mario Bravetti, Gianluigi Zavattaro (Eds.): Proceedings of the First International Workshop on Web Services and Formal Methods, Pisa, Italy, February 2004. Published in: Electronic Notes in Theoretical Computer Science, Volume 105, 10 December 2004, Pages 147-158.
• 4-10.055V
  Friedrich H. Vogt, Simon Zambrovski, Boris Gruschko, Peter Furness, and Alastair Green. Implementing Web Service Protocols in SOA: WS-Coordination and WS-Business Activity. In Proceedings of the 7th IEEE International Conference on E-Commerce Technology Workshops (CEC 2005). München, July 19-22, 2005.
• 4-10.056V
  Boris Gruschko, Friedrich H. Vogt, and Simon Zambrovski. The Use of TLA+ and Model Checking Tools in the Eclipse Environment. In 2nd International Workshop on Web Services and Formal Methods. Versailles, France, September 1-3, 2005.
• 4-10.058V
  Friedrich H. Vogt, and Arsalan Minhas. Using Service Orientation to Drive Business Processes. In Proceedings of the 9th IEEE International Multi Topic conference. Karachi, Pakistan, December 13-25, 2005.

Stichwörter

• Model Checking
• Specification
• Standards
• Temporal Logic of Actions (TLA)
• Verification