Model-Checking of Web Services Choreography

Web services choreography describes the global model of service interactions among a set of participants. In order to achieve a common business goal, the protocols of interaction must be correct. In this paper, we model interactions with recordings of state/channel variable changes that can occur as a result of carrying out the interactions. Thus, it is possible to verify not only normal control flow properties such as deadlock-freeness, but also channel-passing related problems such as channel-absence. Concretely, we propose a small language CDL, together with an operational semantics. We illustrate with a T-Shirts procurement protocol how service choreographies can be specified in CDL, and how the verification can be carried out using the SPIN model-checker.