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　modelchecker.　©　2008　IEEE.