Modelling and Verification of Web Services Business Activity Protocol

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F11%3A00067341" target="_blank" >RIV/00216224:14330/11:00067341 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1007/978-3-642-19835-9_32" target="_blank" >http://dx.doi.org/10.1007/978-3-642-19835-9_32</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-642-19835-9_32" target="_blank" >10.1007/978-3-642-19835-9_32</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Modelling and Verification of Web Services Business Activity Protocol

Popis výsledku v původním jazyce

WS-Business Activity specification defines two coordination protocols in order to ensure a consistent agreement on the outcome of long-running distributed applications. We use the model checker Uppaal to analyse the Business Agreement with Coordination Completion protocol type. Our analyses show that the protocol, as described in the standard specification, violates correct operation by reaching invalid states for all underlying communication media except for the perfect FIFO. Based on this result, we propose changes to the protocol. A further investigation of the modified protocol suggests that messages should be received in the same order as they are sent so that a correct protocol behaviour is preserved. Another important property of communication protocols is that all parties always reach their final states.

Název v anglickém jazyce

Modelling and Verification of Web Services Business Activity Protocol

Popis výsledku anglicky

WS-Business Activity specification defines two coordination protocols in order to ensure a consistent agreement on the outcome of long-running distributed applications. We use the model checker Uppaal to analyse the Business Agreement with Coordination Completion protocol type. Our analyses show that the protocol, as described in the standard specification, violates correct operation by reaching invalid states for all underlying communication media except for the perfect FIFO. Based on this result, we propose changes to the protocol. A further investigation of the modified protocol suggests that messages should be received in the same order as they are sent so that a correct protocol behaviour is preserved. Another important property of communication protocols is that all parties always reach their final states.

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

—

Návaznosti

Z - Vyzkumny zamer (s odkazem do CEZ)

Rok uplatnění

2011

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 statě ve sborníku

Proceedings of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems ({TACAS}'11)

ISBN

9783642198342

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

15

Strana od-do

357-371

Název nakladatele

Springer-Verlag

Místo vydání

Neuveden

Místo konání akce

Saarbrücken, Germany

Datum konání akce

1. 1. 2011

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—