Model Checking Based Approach for Compliance Checking

Organisation:	CNR, Pisa and Napoli (ITALY) University of Molise, Pesche (ITALY) University of Sannio, Benevento (ITALY) University of Pisa (ITALY)
Method:	LOTOS XES (eXtensible Event Stream)
Tools used:	ProM CADP (Construction and Analysis of Distributed Processes)
Domain:	Process Mining.
Period:	2019
Size:	between 2000 and 10000 event traces
Description:	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.
Conclusions:	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 [Martinelli-Mercaldo-Nardone-et-al-19]: "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 correct it".
Publications:	[Martinelli-Mercaldo-Nardone-et-al-19] 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 the CADP Web site in PDF or PostScript
Contact:	Fabio Martinelli 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

Back to the CADP case studies page