Web　services　solve　the　problem　of　inter-organization　business　integration　and　are　under　a　distributed,　dynamic,　autonomic　and　heterogeneous　environment.　The　correctness　and　verification　of　web　service　orchestration　is　important.　Formalization　is　a　valid　method.　This　paper　gives　the　specification　of　web　service　orchestration　based　on　concurrent　transaction　logic.　The　translation　rules　from　WS-BPEL　to　concurrent　transaction　logic　are　given.　The　verification　problem　of　web　service　orchestration　based　on　concurrent　transaction　logic　is　discussed.　Finally,　an　actual　web　service　orchestration　model　based　on　concurrent　transaction　logic　is　illustrated.