CONICET | Buscador de Institutos y Recursos Humanos

The representation of process and service choreographies has been recognized as an important requirement in service-oriented methodologies. The guarantee of alignment between process and service choreographies and the veriﬁcation of the behavior of choreographies represent an important improvement for such methodologies, since they enable the automatic generation of choreography service speciﬁcations from well-deﬁned choreography process models. To deal with these issues, we propose a transformation pattern that guarantees behavior alignment between process and service choreographies, and a veriﬁcation method for the control ﬂow of choreographies, which can be applied to any choreography language. These approaches make use of the Global Interaction Nets (GI-Nets) language to formalize the behavior of process and service choreographies. This formal representation can then be used to conclude on the behavioral aspects of choreographies. In addition, we present a tool for the modeling, automatic generation and veriﬁcation of GI-Nets, and apply the proposed approaches to the UP-ColBPIP and WS-CDL choreography languages.