A formal analysis of the web services atomic transaction protocol with UPPAAL

22Citations
Citations of this article
23Readers
Mendeley users who have this article in their library.
Get full text

Abstract

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. © 2010 Springer-Verlag.

Cite

CITATION STYLE

APA

Ravn, A. P., Srba, J., & Vighio, S. (2010). A formal analysis of the web services atomic transaction protocol with UPPAAL. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6415 LNCS, pp. 579–593). https://doi.org/10.1007/978-3-642-16558-0_47

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free