A Formal Analysis of the Web Services Atomic Transaction Protocol with UPPAAL

Anders Peter Ravn, Jiri Srba, Saleem Vighio

Publikation: Bidrag til tidsskriftKonferenceartikel i tidsskriftForskningpeer review

17 Citationer (Scopus)

Abstrakt

We present a formal analysis of the Web Services Atomic Transaction (WS-AT) protocol. WS-AT is a part of the WS-Coordination framework and describes an algorithm for reaching agreement on the outcome of a distributed transaction. The protocol is modelled and verified using the model checker UPPAAL. Our model is based on an already available formalization using the mathematical language TLA+ where the protocol was verified using the model checker TLC. We discuss the key aspects of these two approaches, including the characteristics of the specification languages, the performances of the tools, and the robustness of the specifications with respect to extensions.
OriginalsprogEngelsk
BogserieLecture Notes in Computer Science
Vol/bind6415
Sider (fra-til)579-593
ISSN0302-9743
DOI
StatusUdgivet - 2010

Fingeraftryk Dyk ned i forskningsemnerne om 'A Formal Analysis of the Web Services Atomic Transaction Protocol with UPPAAL'. Sammen danner de et unikt fingeraftryk.

Citationsformater