ITO, Sohei, Dominik VYMĚTAL and Roman ŠPERKA. Process Mining Approach to Formal Business Process Modelling and Verification: A Case Study. Journal of Modelling in Management. Emerald Group Publishing Ltd., 2020, vol. 16, No 2, p. 1-21. ISSN 1746-5664. Available from: https://dx.doi.org/10.1108/JM2-03-2020-0077.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name Process Mining Approach to Formal Business Process Modelling and Verification: A Case Study
Authors ITO, Sohei (392 Japan, belonging to the institution), Dominik VYMĚTAL (203 Czech Republic, belonging to the institution) and Roman ŠPERKA (703 Slovakia, guarantor, belonging to the institution).
Edition Journal of Modelling in Management, Emerald Group Publishing Ltd. 2020, 1746-5664.
Other information
Original language English
Type of outcome Article in a journal
Field of Study 50204 Business and management
Country of publisher United Kingdom of Great Britain and Northern Ireland
Confidentiality degree is not subject to a state or trade secret
WWW URL
RIV identification code RIV/47813059:19520/20:A0000153
Organization unit School of Business Administration in Karvina
Doi http://dx.doi.org/10.1108/JM2-03-2020-0077
Keywords in English Business process modelling; Computing; Formal method; Modelling; Process mining; Timed automaton
Tags International impact, Reviewed
Changed by Changed by: doc. RNDr. Ing. Roman Šperka, Ph.D., učo 18157. Changed: 9/7/2021 10:22.
Abstract
Purpose: The need for assuring correctness of business processes in enterprises is widely recognised in terms of business process re-engineering and improvement. Formal methods are a promising approach to this issue. The challenge in business process verification is to create a formal model that is well-aligned to the reality. Process mining is a well-known technique to discover a model of a process based on facts. However, no studies exist that apply it to formal verification. This study aims to propose a methodology for formal business process verification by means of process mining, and attempts to clarify the challenges and necessary technologies in this approach using a case study. Design/methodology/approach: A trading company simulation model is used as a case study. A workflow model is discovered from an event log produced by a simulation tool and manually complemented to a formal model. Correctness requirements of both domain-dependent and domain-independent types of the model are checked by means of model-checking. Findings: For business process verification with both domain-dependent and domain-independent correctness requirements, more advanced process mining techniques that discover data-related aspects of processes are desirable. The choice of a formal modelling language is also crucial. It depends on the correctness requirements and the characteristics of the business process. Originality/value: Formal verification of business processes starting with creating its formal model is quite new. Furthermore, domain-dependent and domain-independent correctness properties are considered in the same framework, which is also new. This study revealed necessary technologies for this approach with process mining.
PrintDisplayed: 4/5/2024 20:19