Verification of channel passing in choreography with model checking

A Web service choreography describes a global protocol of interactions among a set of cooperating services. For the dynamic composition, changing interconnections by channel passing between services is necessary. In this paper we use model checking technique for the verifying problems related to channel passing in choreography. We develop a framework: for each kind of property to be verified, we define an abstraction function based on it, which map each basic interaction into a pair of pre- and post-conditions, then propose a compositional approach to translate choreographies into models for model checkers. A number of examples are presented to show how the verification is carried out.