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: