Model-Checking Web Services Business Activity Protocols

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F12%3A00062432" target="_blank" >RIV/00216224:14330/12:00062432 - isvavai.cz</a>

Result on the web

<a href="http://dx.doi.org/10.1007/s10009-012-0231-4" target="_blank" >http://dx.doi.org/10.1007/s10009-012-0231-4</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/s10009-012-0231-4" target="_blank" >10.1007/s10009-012-0231-4</a>

Result language

angličtina

Original language name

Model-Checking Web Services Business Activity Protocols

Original language description

Web Services Business Activity specification defines two coordination protocols BAwCC (Business Agreement with Coordination Completion) and BAwPC (Business Agreement with Participant Completion)that ensure a consistent agreement on the outcome of long-running distributed applications. In order to verify fundamental properties of the protocols we provide formal analyses in the model checker UPPAAL.Our analyses are supported by a newly developed tool chain,where in the first step we translatetables with state-transition protocol descriptionsinto an intermediate XML format, and in the second step we translate this format into a network of communicating state machines directly suitable for verification in UPPAAL.Our results show that the WS-BA protocols, as described in the standard specification, violate correct operation by reaching invalid statesfor all underlying communication media except for a perfect FIFO.

Czech name

—

Czech description

—

Type

J_x - Unclassified - Peer-reviewed scientific article (Jimp, Jsc and Jost)

CEP classification

IN - Informatics

OECD FORD branch

—

Project

<a href="/en/project/LA09016" target="_blank" >LA09016: Czech Republic membership in the European Research Consortium for Informatics and Mathematics (ERCIM)</a><br>

Continuities

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Publication year

2012

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Name of the periodical

International Journal on Software Tools for Technology Transfer (STTT)

ISSN

1433-2779

e-ISSN

—

Volume of the periodical

2012

Issue of the periodical within the volume

1

Country of publishing house

NL - THE KINGDOM OF THE NETHERLANDS

Number of pages

23

Pages from-to

1-23

UT code for WoS article

—

EID of the result in the Scopus database

—