Model-Checking Web Services Business Activity Protocols

Abinoam P. Marques, Anders Peter Ravn, Jiri Srba, Saleem Vighio

Research output: Contribution to journalJournal articleResearchpeer-review

6 Citations (Scopus)

Abstract

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.
Original languageEnglish
JournalInternational Journal on Software Tools for Technology Transfer
Volume15
Issue number2
Pages (from-to)125-147
ISSN1433-2779
DOIs
Publication statusPublished - 2013

Fingerprint

Model checking
Web services
Network protocols
Industry
Specifications
Communication
XML

Keywords

  • web services, verification, timed automata

Cite this

Marques, Abinoam P. ; Ravn, Anders Peter ; Srba, Jiri ; Vighio, Saleem. / Model-Checking Web Services Business Activity Protocols. In: International Journal on Software Tools for Technology Transfer. 2013 ; Vol. 15, No. 2. pp. 125-147.
@article{3bd46e5fc8be4ef2bb5d0aa7f696cc3e,
title = "Model-Checking Web Services Business Activity Protocols",
abstract = "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.",
keywords = "web services, verification, timed automata",
author = "Marques, {Abinoam P.} and Ravn, {Anders Peter} and Jiri Srba and Saleem Vighio",
year = "2013",
doi = "10.1007/s10009-012-0231-4",
language = "English",
volume = "15",
pages = "125--147",
journal = "International Journal on Software Tools for Technology Transfer",
issn = "1433-2779",
publisher = "Springer Publishing Company",
number = "2",

}

Model-Checking Web Services Business Activity Protocols. / Marques, Abinoam P.; Ravn, Anders Peter; Srba, Jiri; Vighio, Saleem.

In: International Journal on Software Tools for Technology Transfer, Vol. 15, No. 2, 2013, p. 125-147.

Research output: Contribution to journalJournal articleResearchpeer-review

TY - JOUR

T1 - Model-Checking Web Services Business Activity Protocols

AU - Marques, Abinoam P.

AU - Ravn, Anders Peter

AU - Srba, Jiri

AU - Vighio, Saleem

PY - 2013

Y1 - 2013

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.

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

KW - web services, verification, timed automata

U2 - 10.1007/s10009-012-0231-4

DO - 10.1007/s10009-012-0231-4

M3 - Journal article

VL - 15

SP - 125

EP - 147

JO - International Journal on Software Tools for Technology Transfer

JF - International Journal on Software Tools for Technology Transfer

SN - 1433-2779

IS - 2

ER -