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

Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F10%3A00045630" target="_blank" >RIV/00216224:14330/10:00045630 - isvavai.cz</a>
Result on the web
—
DOI - Digital Object Identifier
—

Result language
angličtina
Original language name
A Formal Analysis of the Web Services Atomic Transaction Protocol with UPPAAL
Original language description
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 modelledand 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.
Czech name
—
Czech description
—

Project
<a href="/en/project/1M0545" target="_blank" >1M0545: Institute for Theoretical Computer Science</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Publication year
2010
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Article name in the collection
Proceedings of the 4th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISOLA'10)
ISBN
978-3-642-16560-3
ISSN
—
e-ISSN
—
Number of pages
15
Pages from-to
—
Publisher name
Springer
Place of publication
Holland
Event location
Greese
Event date
Jan 1, 2010
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—

Similar results(10)