Tool Supported Analysis of Web Services Protocols

Warning

This publication doesn't include Faculty of Arts. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

MARQUES Abinoam Jr. RAVN Anders P. SRBA Jiří VIGHIO Saleem

Year of publication 2011
Type Article in Proceedings
Conference Proceedings of the 5th International Workshop of Harnessing Theories for Tool Support in Software ({TTSS}'11)
MU Faculty or unit

Faculty of Informatics

Citation
Web http://www.duo.uio.no/sok/work.html?WORKID=137619
Field Informatics
Keywords web services; verification; tool; UPPAAL
Description 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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.