Model-Checking Web Services Business Activity Protocols

Kód výsledku v 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>

Výsledek na webu

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

Jazyk výsledku

angličtina

Název v původním jazyce

Model-Checking Web Services Business Activity Protocols

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Model-Checking Web Services Business Activity Protocols

Popis výsledku anglicky

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.

Druh

J_x - Nezařazeno - Článek v odborném periodiku (Jimp, Jsc a Jost)

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

<a href="/cs/project/LA09016" target="_blank" >LA09016: Účast ČR v European Research Consortium for Informatics and Mathematics (ERCIM)</a><br>

Návaznosti

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

Rok uplatnění

2012

Kód důvěrnosti údajů

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

Název periodika

International Journal on Software Tools for Technology Transfer (STTT)

ISSN

1433-2779

e-ISSN

—

Svazek periodika

2012

Číslo periodika v rámci svazku

1

Stát vydavatele periodika

NL - Nizozemsko

Počet stran výsledku

23

Strana od-do

1-23

Kód UT WoS článku

—

EID výsledku v databázi Scopus

—