Despite the importance for expressing location mobility and dynamic composition, channel passing has almost been ignored in the formal work on Web service composition. One important problem here is to ensure that each service in a composition can always get sufficient and correct channels for completing their collaborative work. To support reasoning and verification of those properties of service compositions, in this paper we propose a pair of formal languages that support channel passing on both global and local levels, together with their semantics. Also we present a top-down design methodology that generates local-level processes from global description, and prove that the generated processes must be deadlock-free under the sufficient conditions we proposed.