Abstract: 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 WSCDL 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.