A Logical Representation and Verification of Web Service Choreography

Web services choreography describes global model of services interactions among a set of participants. The correct description of choreography is very important, so before implementation upon choreography design description, we must be sure about correctness. Several techniques are employed to verif...

Full description

Saved in:
Bibliographic Details
Main Authors: Madani, Z., Nematbakhsh, N., Zamanifar, K., Mardukhi, F.
Format: Conference Proceeding
Language:English
Subjects:
Application software
Automata
Collaboration
Information technology
Logic
Runtime
Software engineering
System recovery
Time factors
Web services
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Web services choreography describes global model of services interactions among a set of participants. The correct description of choreography is very important, so before implementation upon choreography design description, we must be sure about correctness. Several techniques are employed to verify WS-CDL. In this paper we use a logical formal model to verify specifications of WS-CDL. In our approach, we model some important aspects of WS-CDL, such as channel passing, Timeout and policies in first order logic and then use Prolog tool to check reachability of all goal states of choreography interactions.
DOI:10.1109/IITA.2009.289