Verifying Correctness of Web Services Choreography

This paper is about Web services used in distributed, inter-organizational business cooperation (choreography). In this application scenario, we have a multipart functional convention between all the involved Web services (called partners) in order to reach the purpose of the choreography. In such a scenario, two main problems can occur: i) can we determine whether the resulted composition of partner is conforming or not to the expected behavior, with respect to the initial cooperation schema? ii) Can we determine whether the cooperation is possible by considering the individual partners´ behaviors? i.e., are the different partners´ behaviors compatible between them? In this paper, we address the second problem. We propose a method to model partners´ behaviors and to check the correctness of the choreography (deadlock-free) based on the properties of one partner´s behavior