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. Weitere Informationen zu diesem Forschungsprojekt können Sie hier bekommenPublikationen
Stichwörter
| |||||||||||||||