Modelling and Verification of Web Services Business Activity
Protocol

D 2011

Modelling and Verification of Web Services Business Activity Protocol

RAVN, Anders P.; Jiří SRBA a Saleem VIGHIO

Základní údaje

Originální název

Modelling and Verification of Web Services Business Activity Protocol

Název česky

Modelovani a Verifikace WS Business Activity protokolu

Autoři

RAVN, Anders P.; Jiří SRBA a Saleem VIGHIO

Vydání

Neuveden, Proceedings of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems ({TACAS}'11), od s. 357-371, 15 s. 2011

Nakladatel

Springer-Verlag

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Nizozemské království

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

tištěná verze "print"

Odkazy

URL

Impakt faktor

Impact factor: 0.402 v roce 2005

Označené pro přenos do RIV

Ano

Kód RIV

RIV/00216224:14330/11:00067341

Organizační jednotka

Fakulta informatiky

ISBN

978-3-642-19834-2

ISSN

DOI

https://doi.org/10.1007/978-3-642-19835-9_32

UT WoS

000301820100032

Klíčová slova anglicky

verification; modelling; web services; business activity

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 29. 4. 2014 06:30, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

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. Based on the verification with different communication models, we prove that our enhanced protocol satisfies this property for asynchronous, unreliable, order-preserving communication whereas the original protocol does not.

Návaznosti

MSM0021622419, záměr

Název: Vysoce paralelní a distribuované výpočetní systémy

Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy

Citovat

RAVN, Anders P.; Jiří SRBA a Saleem VIGHIO. Modelling and Verification of Web Services Business Activity Protocol. In Proceedings of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems ({TACAS}'11). Neuveden: Springer-Verlag, 2011, s. 357-371. ISBN 978-3-642-19834-2. Dostupné z: https://doi.org/10.1007/978-3-642-19835-9_32.

@inproceedings{963627,
   author = {Ravn, Anders P. and Srba, Jiří and Vighio, Saleem},
   address = {Neuveden},
   booktitle = {Proceedings of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems ({TACAS}'11)},
   doi = {https://doi.org/10.1007/978-3-642-19835-9_32},
   keywords = {verification; modelling; web services; business activity},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Neuveden},
   isbn = {978-3-642-19834-2},
   pages = {357-371},
   publisher = {Springer-Verlag},
   title = {Modelling and Verification of Web Services Business Activity Protocol},
   url = {http://www.springerlink.com/content/978-3-642-19834-2},
   year = {2011}
}

TY  - CONF
ID  - 963627
AU  - Ravn, Anders P. - Srba, Jiří - Vighio, Saleem
PY  - 2011
TI  - Modelling and Verification of Web Services Business Activity Protocol
PB  - Springer-Verlag
CY  - Neuveden
SN  - 9783642198342
KW  - verification
KW  - modelling
KW  - web services
KW  - business activity
UR  - http://www.springerlink.com/content/978-3-642-19834-2
N2  - 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. Based on the verification with different communication models, we prove that our enhanced protocol satisfies this property for asynchronous, unreliable, order-preserving communication whereas the original protocol does not.
ER  -

RAVN, Anders P.; Jiří SRBA a Saleem VIGHIO. Modelling and Verification of Web Services Business Activity Protocol. In \textit{Proceedings of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems ($\{$TACAS$\}$'11)}. Neuveden: Springer-Verlag, 2011, s.~357-371. ISBN~978-3-642-19834-2. Dostupné z: https://doi.org/10.1007/978-3-642-19835-9\_{}32.

Přehled o publikaci