Formalization and verification of event-driven process chains

For many companies, business processes have become the focal point of atten tion. As a result, many tools have been developed for business process engi neering and the actual deployment of business processes. Typical examples o f these tools are Business Process Reengineering (BPR) tools, Enterprise Re source Planning (ERP) systems, and Workflow Management (WFM) systems. Some of the leading products, e.g. SAP R/3 (ERP/WFM) and ARIS (BPR), use Event-d riven Process Chains (EPCs) to model business processes. Although the EPCs have become a widespread process modeling technique, they suffer from a ser ious drawback: neither the syntax nor the semantics of an EPC are well defi ned. Ln this paper, this problem is tackled by mapping EPCs (without connec tors of type v) onto Petri nets. The Petri nets have formal semantics and p rovide an abundance of analysis techniques. As a result, the approach prese nted in this paper gives formal semantics to EPCs. Moreover, many analysis techniques are available for EPCs. To illustrate the approach, it is shown that the correctness of an EPC can be checked in polynomial time by using P etri-net-based analysis techniques. (C) 1999 Elsevier Science B.V. All righ ts reserved.