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 of B2B specifications from collaborative business process models enables enterprises to implement B2B collaborations with their partners, reducing the costs, time and complexity in the generation of technological solutions. Because of collaborative processes describe the behavior of the interactions between the partners, an important issue is the verification of the correctness of these processes, such as the absence of deadlocks and livelocks. In this work we describe how collaborative process models can be verified exploiting the benefits of a MDA approach. We describe the formalization of collaborative process models defined with the UP-ColBPIP language by using Petri Nets and the transformations of UP-ColBPIP models into Petri Nets specifications. Thus, a formal semantics for collaborative process models is provided, which enables the verification of these models through tools for verification of Petri Nets.