Verification of Models in a MDA Approach for Collaborative Business Processes

PABLO VILLARREAL,; JORGE ROA; ENRIQUE SALOMONE; OMAR CHIOTTI,

Venezuela

Workshop; 10º Workshop Iberoamericano de Ingeniería de Requisitos y Ambientes de Software (IDEAS´07); 2007

The application of a MDA approach for the automatic generation ofB2B specifications from collaborative business process models enablesenterprises to implement B2B collaborations with their partners, reducing thecosts, time and complexity in the generation of technological solutions. Becauseof collaborative processes describe the behavior of the interactions between thepartners, an important issue is the verification of the correctness of theseprocesses, such as the absence of deadlocks and livelocks. In this work wedescribe how collaborative process models can be verified exploiting thebenefits of a MDA approach. We describe the formalization of collaborativeprocess models defined with the UP-ColBPIP language by using Petri Nets andthe transformations of UP-ColBPIP models into Petri Nets specifications. Thus,a formal semantics for collaborative process models is provided, which enablesthe verification of these models through tools for verification of Petri Nets.