Web　service　choreography　among　organizations　should　be　established　on　the　basis　of　formal　model.　This　paper　establishes　the　model　of　web　service　choreography　based　on　concurrent　transaction　logic　and　the　translation　rules　from　WS-CDL　to　concurrent　transaction　logic　are　given.　The　concurrent　transaction　model　of　web　service　choreography　is　established　on　the　basis　of　formal　methods　and　is　easy　to　verify　properties　of　web　service　choreography.　Finally,　an　actual　web　service　choreography　model　based　on　concurrent　transaction　logic　is　illustrated.