About: Model-Checking Web Services Business Activity Protocols

Facets (new session)
Description
Metadata
Settings
- owl:sameAs
- Inference Rule:

About: Model-Checking Web Services Business Activity Protocols Goto Sponge NotDistinct Permalink

An Entity of Type : http://linked.opendata.cz/ontology/domain/vavai/Vysledek, within Data Space : linked.opendata.cz associated with source document(s)

Attributes	Values
rdf:type	skos:Concept http://linked.opendata.cz/ontology/domain/vavai/Vysledek
rdfs:seeAlso	http://dx.doi.org/10.1007/s10009-012-0231-4
Description	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. 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. (en)
Title	Model-Checking Web Services Business Activity Protocols Model-Checking Web Services Business Activity Protocols (en)
skos:prefLabel	Model-Checking Web Services Business Activity Protocols Model-Checking Web Services Business Activity Protocols (en)
skos:notation	RIV/00216224:14330/12:00062432!RIV13-MSM-14330___
http://linked.open...avai/riv/aktivita	I P
http://linked.open...avai/riv/aktivity	I, P(LA09016)
http://linked.open...iv/cisloPeriodika	1
http://linked.open...vai/riv/dodaniDat	2013
http://linked.open...aciTvurceVysledku	Srba, Jiří
http://linked.open.../riv/druhVysledku	J - Článek v odborném periodiku
http://linked.open...iv/duvernostUdaju	S - Úplné a pravdivé údaje nepodléhající ochraně podle zvláštních právních předpisů
http://linked.open...titaPredkladatele	Masarykova univerzita / Fakulta informatiky
http://linked.open...dnocenehoVysledku	150967
http://linked.open...ai/riv/idVysledku	RIV/00216224:14330/12:00062432
http://linked.open...riv/jazykVysledku	eng - angličtina
http://linked.open.../riv/klicovaSlova	web services; verification; timed automata (en)
http://linked.open.../riv/klicoveSlovo	verification web services timed automata
http://linked.open...odStatuVydavatele	NL - Nizozemsko
http://linked.open...ontrolniKodProRIV	[41317CC6C7B1]
http://linked.open...i/riv/nazevZdroje	International Journal on Software Tools for Technology Transfer (STTT)
http://linked.open...in/vavai/riv/obor	IN
http://linked.open...ichTvurcuVysledku	1 (xsd:int)
http://linked.open...cetTvurcuVysledku	4 (xsd:int)
http://linked.open...vavai/riv/projekt	Czech Republic membership in the European Research Consortium for Informatics and Mathematics (ERCIM)
http://linked.open...UplatneniVysledku	2012
http://linked.open...v/svazekPeriodika	2012
http://linked.open...iv/tvurceVysledku	Srba, Jiří Vighio, Saleem Marques, Abinoam P. Ravn, Andres P.
issn	1433-2779
number of pages	23 (xsd:int)
http://bibframe.org/vocab/doi	10.1007/s10009-012-0231-4
http://localhost/t...ganizacniJednotka	14330

Faceted Search & Find service v1.16.118 as of Jun 21 2024

Alternative Linked Data Documents: ODE Content Formats:

RDF

ODATA

Microdata

About

OpenLink Virtuoso version 07.20.3240 as of Jun 21 2024, on Linux (x86_64-pc-linux-gnu), Single-Server Edition (126 GB total memory, 112 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software