| Identifikační kód | RIV/00216224:14330/11:00054546 |
|---|
| Název v anglickém jazyce | Tool Supported Analysis of Web Services Protocols |
|---|
| Druh | D - Článek ve sborníku |
|---|
| Jazyk | eng - angličtina |
|---|
| Obor - skupina | I - Informatika |
|---|
| Obor | IN - Informatika |
|---|
| Rok uplatnění | 2011 |
|---|
| Kód důvěrnosti údajů | S - Úplné a pravdivé údaje o výsledku nepodléhající ochraně podle zvláštních právních předpisů. |
|---|
| Počet výskytů výsledku | 1 |
|---|
| Počet tvůrců celkem | 4 |
|---|
| Počet domácích tvůrců | 1 |
|---|
| Výčet všech uvedených jednotlivých tvůrců | Abinoam Jr. Marques (státní příslušnost: BR - Brazilská federativní republika)
Anders P. Ravn (státní příslušnost: DK - Dánské království)
Jiří Srba (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 2753057)
Saleem Vighio (státní příslušnost: PK - Pákistánská islámská republika) |
|---|
| Popis výsledku v anglickém jazyce | We describe an abstract protocol model suitable for modelling of web services and other protocols communicating via unreliable, asynchronous communication channels. The model is supported by a tool chain where the first step translates tables with state/transition protocol descriptions, often used e.g. in the design of web services protocols, into an intermediate XML format. We further translate this format into a network of communicating state machines directly suitable for verification in the model checking tool UPPAAL. We introduce two types of communication media abstractions in order to ensure the finiteness of the protocol state-spaces while still being able to verify interesting protocol properties. The translations for different kinds of communication media have been implemented and successfully tested, among others, on agreement protocols from WS-Business Activity. |
|---|
| Klíčová slova oddělená středníkem | web services; verification; tool; UPPAAL |
|---|
| Stránka www, na které se nachází výsledek | - |
|---|