Formalizing Business Process Execution Language Based on Petri Nets

Formalizing and verifying Web service composition is one important research area in service oriented computing (SOC). In order to design Business Processes specified by business process execution language (BPEL) correctly, and make ensure it can run accurately, an extended Petri-net model with labels and two colored tokens is proposed to formalize BPEL process. The formal model focuses on specifying the concept of partner, control link, death path elimination (DPE), etc. Labels are used to specify variables, partners and their operations. Two colors tokens, TRUE and FALSE, are used to express true execution, skip execution, and skip signal transfers. The definition for a BPEL process is given by tuples. For specifying semantics of the model, the concepts, such as external transition sequence, are presented for providing a basis of simulation and analysis.