We propose a technique to automatically generate a formal specification of the model of a system from a set of observations of its behaviour. We aim to free systems modellers from the burden of explicitly formalising the behaviour of an existing system to analyse it. We take advantage of an algorithm introduced by the process mining community, which takes as input an event log and generates a formal specification that can be combined with other specifications to obtain a global model of the overall behaviour of a system. Specifically, we have adapted a known process discovery algorithm to produce a specification in mCRL2, a formal specification language based on process algebras. The availability of mCRL2 specifications enables us to take advantage of its rich toolset for verifying systems properties and for effectively reasoning over distributed scenarios where multiple organizations interact to reach common goals. This is an aspect that is not supported by the approaches based on Petri Nets, usually used for process mining. The methodology has been integrated in a stand-alone tool and has been validated using custom-made and real event logs.

PALM: A Technique for Process ALgebraic Specification Mining

Belluccini S.;De Nicola R.;Re B.;Tiezzi F.
2020

Abstract

We propose a technique to automatically generate a formal specification of the model of a system from a set of observations of its behaviour. We aim to free systems modellers from the burden of explicitly formalising the behaviour of an existing system to analyse it. We take advantage of an algorithm introduced by the process mining community, which takes as input an event log and generates a formal specification that can be combined with other specifications to obtain a global model of the overall behaviour of a system. Specifically, we have adapted a known process discovery algorithm to produce a specification in mCRL2, a formal specification language based on process algebras. The availability of mCRL2 specifications enables us to take advantage of its rich toolset for verifying systems properties and for effectively reasoning over distributed scenarios where multiple organizations interact to reach common goals. This is an aspect that is not supported by the approaches based on Petri Nets, usually used for process mining. The methodology has been integrated in a stand-alone tool and has been validated using custom-made and real event logs.
978-3-030-63460-5
978-3-030-63461-2
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11581/453030
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? ND
social impact