Model-Checking Web Services Business Activity Protocols

J 2012

Model-Checking Web Services Business Activity Protocols

MARQUES, Abinoam P.; Andres P. RAVN; Jiří SRBA a Saleem VIGHIO

Základní údaje

Originální název

Model-Checking Web Services Business Activity Protocols

Autoři

MARQUES, Abinoam P.; Andres P. RAVN; Jiří SRBA a Saleem VIGHIO

Vydání

International Journal on Software Tools for Technology Transfer (STTT), 2012, 1433-2779

Další údaje

Jazyk

angličtina

Typ výsledku

Článek v odborném periodiku

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í

Odkazy

Web

Označené pro přenos do RIV

Ano

Kód RIV

RIV/00216224:14330/12:00062432

Organizační jednotka

Fakulta informatiky

DOI

https://doi.org/10.1007/s10009-012-0231-4

Klíčová slova anglicky

web services; verification; timed automata

Změněno: 23. 4. 2013 09:38, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

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. Hence we propose changes to the protocols and a further investigation of the modified protocols suggests that in case of the BAwCC protocol messages should be received in the same order as they are sent to preserve correct behaviour,while BAwPC is now correct even for asynchronous,unordered, lossy and duplicating media.Another important property of communication protocols is that all parties always reach, under certain fairness assumptions, their final states. Based on an automatic verification with different communication models, we prove that our enhanced protocols satisfy this property whereas the original protocols do not.All verification results presented in this article were performedin a fully automatic way using our new tool csv2uppaal.

Návaznosti

LA09016, projekt VaV

Název: Účast ČR v European Research Consortium for Informatics and Mathematics (ERCIM) (Akronym: ERCIM)

Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Účast ČR v European Research Consortium for Informatics and Mathematics

Citovat

MARQUES, Abinoam P.; Andres P. RAVN; Jiří SRBA a Saleem VIGHIO. Model-Checking Web Services Business Activity Protocols. International Journal on Software Tools for Technology Transfer (STTT). 2012, roč. 2012, č. 1, s. 1-23. ISSN 1433-2779. Dostupné z: https://doi.org/10.1007/s10009-012-0231-4.

@article{1079132,
   author = {Marques, Abinoam P. and Ravn, Andres P. and Srba, Jiří and Vighio, Saleem},
   article_number = {1},
   doi = {https://doi.org/10.1007/s10009-012-0231-4},
   keywords = {web services; verification; timed automata},
   language = {eng},
   issn = {1433-2779},
   journal = {International Journal on Software Tools for Technology Transfer (STTT)},
   title = {Model-Checking Web Services Business Activity Protocols},
   url = {http://dx.doi.org/10.1007/s10009-012-0231-4},
   volume = {2012},
   year = {2012}
}

TY  - JOUR
ID  - 1079132
AU  - Marques, Abinoam P. - Ravn, Andres P. - Srba, Jiří - Vighio, Saleem
PY  - 2012
TI  - Model-Checking Web Services Business Activity Protocols
JF  - International Journal on Software Tools for Technology Transfer (STTT)
VL  - 2012
IS  - 1
SP  - 1-23
EP  - 1-23
SN  - 14332779
KW  - web services
KW  - verification
KW  - timed automata
UR  - http://dx.doi.org/10.1007/s10009-012-0231-4
L2  - http://dx.doi.org/10.1007/s10009-012-0231-4
N2  - 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. Hence we propose changes to the protocols and a further investigation of the modified protocols suggests that in case of the BAwCC protocol messages should be received in the same order as they are sent to preserve correct behaviour,while BAwPC is now correct even for asynchronous,unordered, lossy and duplicating media.Another important property of communication protocols is that all parties always reach, under certain fairness assumptions, their final states. Based on an automatic verification with different communication models, we prove that our enhanced protocols satisfy this property whereas the original protocols do not.All verification results presented in this article were performedin a fully automatic way using our new tool csv2uppaal.
ER  -

MARQUES, Abinoam P.; Andres P. RAVN; Jiří SRBA a Saleem VIGHIO. Model-Checking Web Services Business Activity Protocols. \textit{International Journal on Software Tools for Technology Transfer (STTT)}. 2012, roč.~2012, č.~1, s.~1-23. ISSN~1433-2779. Dostupné z: https://doi.org/10.1007/s10009-012-0231-4.

Přehled o publikaci