In this paper we present the integration of BProVe - Business Process Verifier - into the Apromore opensource process analytics platform. Given a BPMN model BProVe enables the verification of properties such as soundness and safeness. Differently from established techniques for BPMN verification, that rely on the availability of a mapping into a transition based formalism (e.g. Petri Nets), BProVe takes advantage of a direct formalisation of the BPMN semantics in terms of Structural Operational Semantics rules. On the one side, this still permits to give precise meaning to BPMN models, otherwise impossible due to the usage of natural language in the BPMN standard specification. On the other side, it permits to overcome some issues related to the mapping of BPMN to other formal languages equipped with their own semantics (e.g. non local effects of BPMN elements such as termination). The defined BPMN semantics has been implemented in MAUDE. Through the MAUDE Linear Temporal Logic (LTL) model checker, correctness properties encoded in LTL formulae are evaluated and the result is then presented to the user. The integration into Apromore allows model designers to use the Apromore BPMN editor to design models and to interact with BProVe to verify properties of the designed model. The results are shown graphically on top of the process model, so as to highlight behavioural paths that violate the correctness properties. Designers can then easily identify the violation and repair the model accordingly.

Checking Business Process Correctness in Apromore

Fabrizio Fornari;Andrea Polini;Barbara Re;Francesco Tiezzi
2018-01-01

Abstract

In this paper we present the integration of BProVe - Business Process Verifier - into the Apromore opensource process analytics platform. Given a BPMN model BProVe enables the verification of properties such as soundness and safeness. Differently from established techniques for BPMN verification, that rely on the availability of a mapping into a transition based formalism (e.g. Petri Nets), BProVe takes advantage of a direct formalisation of the BPMN semantics in terms of Structural Operational Semantics rules. On the one side, this still permits to give precise meaning to BPMN models, otherwise impossible due to the usage of natural language in the BPMN standard specification. On the other side, it permits to overcome some issues related to the mapping of BPMN to other formal languages equipped with their own semantics (e.g. non local effects of BPMN elements such as termination). The defined BPMN semantics has been implemented in MAUDE. Through the MAUDE Linear Temporal Logic (LTL) model checker, correctness properties encoded in LTL formulae are evaluated and the result is then presented to the user. The integration into Apromore allows model designers to use the Apromore BPMN editor to design models and to interact with BProVe to verify properties of the designed model. The results are shown graphically on top of the process model, so as to highlight behavioural paths that violate the correctness properties. Designers can then easily identify the violation and repair the model accordingly.
2018
978-3-319-92901-9
273
File in questo prodotto:
File Dimensione Formato  
CAiSE2018_Forum.pdf

solo gestori di archivio

Tipologia: Documento in Pre-print
Licenza: NON PUBBLICO - Accesso privato/ristretto
Dimensione 273.09 kB
Formato Adobe PDF
273.09 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

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: https://hdl.handle.net/11581/408053
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? 1
social impact