National University of Defense Technology
Web services composition is an emerging paradigm for enabling application integration within and across organizational boundaries. Business Process Execution Language (BPEL) is a promising language describing the Web services composition in form of business processes, but lack of a sound formal semantic, which hinders the formal analysis and verification of business processes specified in it. This paper presents the transformation of BPEL to Colored Petri nets (CP-nets) in a constructive way. Therefore the authors can translate composition specified in BPEL into CP-nets, which can be analyzed and verified by many specialized tools.