Model-Checking of Web Services Choreography

Abstract 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 examples how service choreographies can be specified in CDL, and how the verification can be carried out using the SPIN model-checker.

• Type: Conference
• Year: 2008
• Where: SOSE
• Authors: Hongli Yang, Xiangpeng Zhao, Chao Cai, Zongyan Qiu
• Keywords: Common Business Goal, Internet Technology, SOSE 2008, State/channel Variable Changes, Web Services Choreography