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