Conceptual business process models such as Event-driven Process Chains (EPCs) play an important role in the business process management life cycle. Since they are often used as an early formalization of process requirements, they should be subject to quality assurance in order to avoid costly rework in later in the implementation phase [9,11]. Verification is related to one particular quality aspect, namely, that business process models should guarantee that every case can be processed with a proper completion. In comparison to other business process modeling languages that are based on Petri nets, EPCs have to features that makes it difficult to do verification with standard Petri net technologies. Firstly, EPCs may have multiple start and end events. Since Soundness [1], as a prominent correctness criterion, is only defined for Workflow nets, i.e. a Petri net class with exactly one source and one sink, it is not directly applicable for EPCs. Secondly, EPCs may have OR-join connectors representing conditional synchronization semantics. Some of these verification challenges have been addressed with the relaxed soundness criterion, and a mapping of EPCs to Petri nets as defined in [3]. Still, proper completion is not guaranteed for a relaxed sound EPC.
For this demonstration we take the novel EPC semantics definition and a corresponding notion of EPC soundness as a starting point (see [7,6]). EPC soundness basically requires (1) that there is a set of initial markings such that every start event is included in at least one of these initial markings, (2) that for every marking, that is reachable from a marking in the set of initial markings, there exists a final marking that can be reached, and (3) that final markings are the only markings reachable from a marking in the set of initial markings such that no node can fire [6, p.106]. In Section 2, we briefly sketch the functionality of xoEPC and discuss its different outputs. In Section 3 illustrate the plug-in that calculates the reachability graph for an EPC, and gives the result of the verification of EPC soundness. Section 4 summarizes the paper.
xoEPC a tool for EPC verification based on reduction rules. 1 It is written in the objectoriented scripting language XOTcl [10], which is an extension of Tcl. xoEPC loads all *.xml files from the current directory and checks whether they are ARIS XML files [4]. If they are, the XML is processed with the tDOM package, a Tcl implementation of the DOM specification. 2 For each EPC model that has at least one event and one function, xoEPC checks syntactical correctness and applies the reduction algorithm. The internal data structure of xoEPC uses an adjacency matrix representation of the EPC, and the reduction methods work on this data structure. xoEPC produces three types of files:
1. All EPCs that cannot be reduced completely are written to the reducedEPCs.epml file. These EPCs can be further analyzed by tools that can read EPML [8].
2. Errors encountered by reduction rules are recorded in the errorresults.xml file. This file also records the processing time of the reduction, metadata of the model, as well as the size of the original and the size of the reduced EPC.
3. Finally, an XHTML file with an embedded SVG graphic3 is generated for each EPC based on the position information in the ARIS XML file. It projects the errors back to the model by highlighting the involved connectors.
The advantages of xoEPC are the following four points. Firstly, due to its reduction rule approach it is performative, providing a result for many EPCs within less than one second [6]. Secondly, since it is based on EPC soundness, it returns a precise result also for EPCs with multiple start and end events as well as with OR-joins. Thirdly, the program runs in a batch mode, and is therefore able to analyze not only one, but several EPC models, without user interaction. Finally, xoEPC projects the errors back onto the visual model such that they can be easily corrected. Still, it might happen that the original EPC is not reduced completely. In this case, the partially reduced EPC can be further analyzed with ProM by importing the reducedEPCs.epml file.
Based on the EPC semantics defined in [6], we have implemented a conversion plug-in for the ProM (Process Mining) framework [2]. ProM was originally developed as a tool for process mining, but meanwhile its functionality was extended to include other types of analysis, model conversions, model comparison, etc. This was enabled by the plugable architecture of ProM, that allows to add new functionality without changing the framework itself, and the fact that ProM supports multiple modeling languages. Since ProM can interact with a variety of existing workflow management systems, simulation tools, ERP systems, and analysis tools (cf. [2]), the plug-in for the new EPC semantics can easily be used for the analysis of existing models. Currently, there are more than 150 plug-ins in release 4.1. ProM basically supports five kinds of plug-ins for mining, importing, exporting, conversion, and analysis. The conversion plug-in maps an EPC to the transition systems package that was developed for an implementation of the incremental workflow mining approach by Kindler, Rubin, and Schäfer [5]. Figure 1 illustrates how the conversion plug-in works. First, one has to load an EPC business process model into ProM, for instance, by using the import plug-in for the ARIS XML format [4] or for the EPC Markup Language [8]. In the figure, the EPC example model for a loan request process is loaded. Since ProM generates a new layout automatically, the model might look different compared to the original layout. Once the EPC is displayed in ProM, one can click on it, trigger the conversion plug-in "EPC to State/Context Transition System", and the reachability graph is calculated and shown in a new ProM window. The dense network of states and transitions on the right-hand side stems from the concurrent execution, if there is both a positive risk assessment for the loan request and the requester is a new customer. There are two markings that do not serve as a source for another transition in case if the request is rejected or accepted. Both these markings are displayed with a green border since they are proper final markings. If they were deadlocks, they would be drawn with a red border. The advantage of the reachability graph analysis is that the result is complete.
In this demonstration, we have presented a combination of two tools for the verification of EPCs. Firstly, xoEPC provides a fast analysis of EPCs with the shortcoming that not all EPCs might be reduced completely. In a second step, only partially reduced EPCs can be further analyzed with a ProM plug-in that explicitly calculates the reachability graph. Since partially reduced EPCs tend to be quite small [6], this combination of tools efficiently circumvents the state explosion problem frequently encountered in process model verification. Further details on both tools are reported in [6].