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

Warning

This publication doesn't include Faculty of Arts. It includes Faculty of Informatics. Official publication website can be found on muni.cz.

Authors	RAVN P. Anders SRBA Jiří VIGHIO Saleem
Year of publication	2010
Type	Article in Proceedings
Conference	Proceedings of the 4th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISOLA'10)
MU Faculty or unit	Faculty of Informatics
Citation
Doi	http://dx.doi.org/10.1007/978-3-642-16558-0_47
Field	Informatics
Keywords	web services protocols; verification; atomic transaction; UPPAAL
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 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.
Related projects:	Institute for Theoretical Computer Science