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

Anders Peter Ravn; Jiri Srba; Saleem Vighio

doi:10.1007/978-3-642-16558-0_47

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

Anders Peter Ravn, Jiri Srba, Saleem Vighio

Department of Computer Science

Research output: Contribution to journal › Conference article in Journal › Research › peer-review

22 Citations (Scopus)

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.

Original language	English
Book series	Lecture Notes in Computer Science
Volume	6415
Pages (from-to)	579-593
ISSN	0302-9743
DOIs	https://doi.org/10.1007/978-3-642-16558-0_47
Publication status	Published - 2010

Access to Document

10.1007/978-3-642-16558-0_47

AUB Link

Search for the material in Aalborg University Library's search engine

Cite this

@inproceedings{1475de0cdd1d4a1ab40b485021818b46,

title = "A Formal Analysis of the Web Services Atomic Transaction Protocol with UPPAAL",

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. ",

author = "Ravn, {Anders Peter} and Jiri Srba and Saleem Vighio",

year = "2010",

doi = "10.1007/978-3-642-16558-0_47",

language = "English",

volume = "6415",

pages = "579--593",

journal = "Lecture Notes in Computer Science",

issn = "0302-9743",

publisher = "Physica-Verlag",

}

TY - GEN

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

AU - Ravn, Anders Peter

AU - Srba, Jiri

AU - Vighio, Saleem

PY - 2010

Y1 - 2010

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-642-16558-0_47

DO - 10.1007/978-3-642-16558-0_47

M3 - Conference article in Journal

SN - 0302-9743

VL - 6415

SP - 579

EP - 593

JO - Lecture Notes in Computer Science

JF - Lecture Notes in Computer Science

ER -

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

Abstract

Access to Document

AUB Link

Fingerprint

Cite this