Transformation of BPMN models for Behaviour Analysis.pdf

Transformation of BPMN models for Behaviour Analysis 1 1 1 Ivo Raedts , Marija Petković , Yaroslav S. Usenko , 1 1 1 Jan Martijn van der Werf , Jan Friso Groote , Lou Somers 1 LaQuSo, Laboratory for Quality Software, an activity of Technische Universiteit Eindhoven and Radboud Universiteit Nijmegen, P.O Box 513, 5600 MB Eindhoven, The Netherlands { i.raedts m.petkovic, y.s.usenko, j.m.v.d.werf, j.f.groote, l.somers }@ Abstract. In industry, many business processes are modelled and stored in En- terprise Information Systems (EIS). Tools supporting the verification and vali- dation of business processes can help to improve the quality of these business processes. However, existing tools can not directly be applied to models used in industry. In this paper, we present our approach for model verification and validation: translating industrial models to Petri nets and mCRL2, and subsequently apply- ing existing tools on the models derived from the initial industrial models. The following translations are described: BPMN models to Petri nets and Petri nets to mCRL2. It is shown what the analysis on the derived models can reveal about the original models. 1 Introduction New laws, standards and technologies have given the use of Enterprise Information Systems (EIS) an enormous boost. For mayor firms, the knowledge about business processes is a mayor asset and is stored in EIS. Different firms define their bus