Business process analysis is one of the most important and complex activity of business process management. Business processes are tipically defined by business experts which ask for graphical and user-friendly notations. Nevertheless used notations tipically lack of precisely defined semantic limiting the possibility of analysis to informal approaches such as observation techniques. To support formal verification techniques it is necessary to define a precise mapping between the adopted user-friendly notation and a formal language.
We propose a Java based verification approach for business processes modeled using the BPMN 2.0 standard. In particular, we defined a precise mapping for each element of the BPMN 2.0 notation to Java. The relations among the different elements of a BPMN 2.0 specification are supported by the inclusion of specific attributes and methods in the created Java objects. The behavior of a set of interrelated objects, corresponding to a BPMN 2.0 specification, can be explored using an algorithm we defined for the purpose. Such an algorithm permits to avoid the state explosion phenomenon using an ad-hoc unfolding technique.
A plug-in for the Eclipse IDE platform has been developed. It is named Cowslip and it is freely available on sourceforge. It permits to have an integrated environment in which to design a business process, to verify it and to check the result of the verification in order to improve the business process itself.
For more information:
- Damiano Falcioni, Andrea Polini, Alberto Polzonetti and Barbara Re. Direct verification of BPMN processes through an optimized unfolding technique, QSIC 2012 – 12th International Conference on Quality Software, in Xi’an, China, 27th – 29th Aug 2012, pp. 179-188.
- Damiano Falcioni, Andrea Polini, Alberto Polzonetti and Barbara Re. Livelock and Deadlock Detection for PA Inter-organizational Business Processes, EGOVIS-EDEM 2012, LNCS 7452, pp 125 – 139, Vienna, Austria, September 3 – 7, 2012.