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

Anders Peter Ravn, Jiri Srba, Saleem Vighio

Publikation: Bidrag til tidsskriftKonferenceartikel i tidsskriftForskningpeer review

17 Citationer (Scopus)

Resumé

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.
OriginalsprogEngelsk
BogserieLecture Notes in Computer Science
Vol/bind6415
Sider (fra-til)579-593
ISSN0302-9743
DOI
StatusUdgivet - 2010

Fingerprint

Formal Analysis
Web services
Web Services
Transactions
Network protocols
Specification languages
Specification Languages
Formalization
Model
Specification
Robustness
Specifications

Citer dette

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

}

A Formal Analysis of the Web Services Atomic Transaction Protocol with UPPAAL. / Ravn, Anders Peter; Srba, Jiri; Vighio, Saleem.

I: Lecture Notes in Computer Science, Bind 6415, 2010, s. 579-593.

Publikation: Bidrag til tidsskriftKonferenceartikel i tidsskriftForskningpeer review

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

VL - 6415

SP - 579

EP - 593

JO - Lecture Notes in Computer Science

JF - Lecture Notes in Computer Science

SN - 0302-9743

ER -