Channel　passing　is　a　mechanism　to　describe　dynamic　composition　of　parallel　systems.　As　to　Web　services,　both　WS-BPEL　and　WS-CDL　adopts　this　mechanism　to　support　dynamic　business　processes.　Web　service　composition　may　suffer　from　channel　passing,　e.g.,　some　service　might　not　get　a　correct　channel　to　complete　an　interaction,　and　then　the　whole　system　would　get　stuck.　The　work　presented　here　is　aimed　at　designing　services　which　are　immune　to　channel　problems.　Firstly,　we　define　a　pair　of　model　languages　on　both　global　and　local　levels　with　formally　defined　semantics.　Based　on　these　languages,　we　propose　a　top-down　design　methodology　that　generates　local-level　processes　from　a　global　specification.　Finally,　we　give　out　a　set　of　conditions　for　global　specifications,　from　which　the　generated　processes　are　guaranteed　correct.　©　2008　Springer　Berlin　Heidelberg.