Behavior Alignment and Control Flow Veri_cation of Process and Service Choreographies [Indexed SCI, IF JCR 2012: 0.762]

ROA, JORGE; DAVID VILLARREAL, PABLO; CHIOTTI, OMAR

JOURNAL OF UNIVERSAL COMPUTER SCIENCE

GRAZ UNIV TECHNOLGOY

Lugar: Graz; Año: 2012 p. 1 - 10

0948-695X

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.