BPMN collaboration models are commonly used to describe the behaviour and interactions of processes in an inter-organisational context. An important role in this kind of models is played both by the message flow, and by sub-processes. The interplay between these features of BPMN models can conceal subtle or unexpected effects, which makes the design activity error-prone, thus leading to the possible inclusion of incorrect behaviour. In this paper, we face this problem by providing a framework for checking the correctness of BPMN models. In particular we are interested on collaboration models that include message exchange and/or sub-processes, and with a special focus on properties well-established in the business process domain, namely safeness and soundness. To enable such a verification, we have (i) defined an operational semantics for BPMN collaborations, (ii) formalised safeness and soundness properties, and a new relaxed version of soundness for detecting situations where asynchronous messages are not handled correctly by the receiver, (iii) applied the related checks on state-space representations (i.e., labelled transition systems) of collaborations, and (iv) implemented the overall formal framework that has been also integrated in the Camunda modelling environment. The resulting verification framework and tool, named S3, have been validated in relation to its effectiveness, efficiency and usability, both by using models available on a publicly accessible repository, and by carrying out experiments with a group of designers.

Correctness checking for BPMN collaborations with sub-processes

Corradini Flavio;Morichetta Andrea
;
Re Barbara;Rossi Lorenzo;
2020-01-01

Abstract

BPMN collaboration models are commonly used to describe the behaviour and interactions of processes in an inter-organisational context. An important role in this kind of models is played both by the message flow, and by sub-processes. The interplay between these features of BPMN models can conceal subtle or unexpected effects, which makes the design activity error-prone, thus leading to the possible inclusion of incorrect behaviour. In this paper, we face this problem by providing a framework for checking the correctness of BPMN models. In particular we are interested on collaboration models that include message exchange and/or sub-processes, and with a special focus on properties well-established in the business process domain, namely safeness and soundness. To enable such a verification, we have (i) defined an operational semantics for BPMN collaborations, (ii) formalised safeness and soundness properties, and a new relaxed version of soundness for detecting situations where asynchronous messages are not handled correctly by the receiver, (iii) applied the related checks on state-space representations (i.e., labelled transition systems) of collaborations, and (iv) implemented the overall formal framework that has been also integrated in the Camunda modelling environment. The resulting verification framework and tool, named S3, have been validated in relation to its effectiveness, efficiency and usability, both by using models available on a publicly accessible repository, and by carrying out experiments with a group of designers.
2020
File in questo prodotto:
File Dimensione Formato  
1-s2.0-S0164121220300716-main (1).pdf

solo gestori di archivio

Tipologia: Versione Editoriale
Licenza: NON PUBBLICO - Accesso privato/ristretto
Dimensione 2.9 MB
Formato Adobe PDF
2.9 MB 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/436971
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 13
  • ???jsp.display-item.citation.isi??? 13
social impact