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

Institut for Datalogi

Publikation: Bidrag til tidsskrift › Konferenceartikel i tidsskrift › Forskning › peer review

22 Citationer (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.

Originalsprog	Engelsk
Bogserie	Lecture Notes in Computer Science
Vol/bind	6415
Sider (fra-til)	579-593
ISSN	0302-9743
DOI	https://doi.org/10.1007/978-3-642-16558-0_47
Status	Udgivet - 2010

Adgang til dokumentet

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

AUB Link

Søg efter materialet i Aalborg Universitetsbiblioteks søgemaskine

Citationsformater

@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

Adgang til dokumentet

AUB Link

Fingeraftryk

Citationsformater