CNR, Pisa and Napoli (ITALY)
University of Molise, Pesche (ITALY)
University of Sannio, Benevento (ITALY)
University of Pisa (ITALY)
XES (eXtensible Event Stream)
CADP (Construction and Analysis of Distributed Processes)
between 2000 and 10000 event traces
Process mining techniques aim at discovering real processes by
extracting knowledge from event logs readily available in information
systems. One of the difficulties faced by process mining is the high
quantity of additional constraints that have to be imposed on the
system to guarantee the needed properties. Compliance refers to the
adherence of the discovered process to internal rules (management
directives, policies, standards) or external rules (laws, regulations,
industry standards). Compliance checking is an important part of the
process mining methodology, and is also a strong requirement in the
context of internal or external audits. The verification of compliance
can be carried out using model checking techniques, by building a
formal model of system starting from its execution traces.
Two compliance checking approaches are proposed. The first one, called integrated-tool approach, uses existing tools, such as the process mining environment ProM and the CADP verification toolbox. After extracting the execution traces from a software system, an LTS (labelled transition system) is obtained using the Mine Transition System plugin of ProM. Then, this LTS is analyzed by checking temporal logic properties using CADP. The approach was applied to a realistic banking transaction process, by considering six scenarios containing between 2000 and 10000 event traces, six temporal properties checked on the LTS, and eight additional properties checked on each trace.
Since the models models discovered through classical process mining techniques can be large and complex, a second, custom-made approach was proposed, which instead of using ProM, defines an algorithm producing abstracted models from execution traces. The abstraction is based on the temporal logic formulas specifying the system properties, which are a declarative representation of the internal and external rules. From the set of abstracted traces, a process described in LOTOS is discovered and used for compliance checking using CADP: the process is compliant with the given rules if it satisfies the corresponding temporal formulas. The approach has been applied on several case-studies: a manufacturing system, a telephone repair process, student careers at University of Pisa, WABO (building permit application process), showing reductions up to 99% in the state space size and verification time w.r.t. the tool-integrated approach.
This work proposes an approach to compliance checking through model
checking. The approach aims at discovering a process described by
means of a process algebra language, while the compliance rules
are defined through temporal logic properties.
The approach uses CADP as model checking engine, as stated in
"We exploit CADP since it is a popular toolbox maintained, regularly
improved, and used in many industrial projects, as a verification
framework. Another important advantage of using CADP is that, when
a property does not hold, the model checking algorithm generates a
counter-example, i.e., an execution trace leading to a state in which
the property is violated. This ability to generate counter-examples
can be exploited to pinpoint the cause of an error and possibly
Fabio Martinelli, Francesco Mercaldo, Vittoria Nardone, Albina Orlando,
Antonella Santone, and Gigliola Vaglini.
"Model Checking Based Approach for Compliance Checking".
Journal of Information Technology and Control 48(2):278-298, 2019.
Available on-line at: http://itc.ktu.lt/index.php/ITC/article/view/21724/12638
or from our FTP site in PDF or PostScript
Istituto di Informatica e Telematica - IIT
Area della Ricerca CNR di Pisa
Via. G. Moruzzi 1
56124 Pisa, Italy
Tel: +39 (0)50 315 3425
Fax: +39 (0)50 315 2593
Email: fabio.martinelli at iit.cnr.it
|Further remarks:||This case-study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|