Automated simulation and verification of process models discovered by process mining
Autor: | Bruno Blašković, Frano Skopljanac-Macina, Ivona Zakarija |
---|---|
Rok vydání: | 2020 |
Předmět: |
FOS: Computer and information sciences
iot 0209 industrial biotechnology Process modeling General Computer Science Computer Science - Artificial Intelligence Computer science lcsh:Automation lcsh:Control engineering systems. Automatic machinery (General) Process mining 02 engineering and technology computer.software_genre lcsh:TJ212-225 Computer Science - Software Engineering IoT model checking inductive machine learning Big Data MAS 020901 industrial engineering & automation mas Linear temporal logic big data 0202 electrical engineering electronic engineering information engineering SPIN model checker lcsh:T59.5 Data stream mining Event (computing) Multi-agent system process mining 020208 electrical & electronic engineering Business process modeling Formal methods Software Engineering (cs.SE) Artificial Intelligence (cs.AI) Control and Systems Engineering Data mining computer |
Zdroj: | Automatika, Vol 61, Iss 2, Pp 312-324 (2020) Automatika : časopis za automatiku, mjerenje, elektroniku, računarstvo i komunikacije Volume 61 Issue 2 |
ISSN: | 1848-3380 0005-1144 |
Popis: | This paper presents a novel approach for automated analysis of process models discovered using process mining techniques. Process mining explores underlying processes hidden in the event data generated by various devices. Our proposed Inductive machine learning method was used to build business process models based on actual event log data obtained from a hotel's Property Management System (PMS). The PMS can be considered as a Multi Agent System (MAS) because it is integrated with a variety of external systems and IoT devices. Collected event log combines data on guests stay recorded by hotel staff, as well as data streams captured from telephone exchange and other external IoT devices. Next, we performed automated analysis of the discovered process models using formal methods. Spin model checker was used to simulate process model executions and automatically verify the process model. We proposed an algorithm for the automatic transformation of the discovered process model into a verification model. Additionally, we developed a generator of positive and negative examples. In the verification stage, we have also used Linear temporal logic (LTL) to define requested system specifications. We find that the analysis results will be well suited for process model repair. 12 pages, 13 figures and 3 tables, published in Automatika, vol. 61, no. 2, pp.312-324, 2020 |
Databáze: | OpenAIRE |
Externí odkaz: |