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　model　of　web　service　orchestration　based　oil　concurrent　transaction　logic.　Ail　introduction　of　web　service　orchestration　and　concurrent　transaction　logic　is　given.　Then　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　example　based　on　concurrent　transaction　logic　is　illustrated.