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 F.; Morichetta A.; Polini A.; Re B.; Rossi L.; Tiezzi F.. - In: THE JOURNAL OF SYSTEMS AND SOFTWARE. - ISSN 0164-1212. - 166:(2020). [10.1016/j.jss.2020.110594]

Correctness checking for BPMN collaborations with sub-processes

Tiezzi F.
2020

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
166
Corradini F.; Morichetta A.; Polini A.; Re B.; Rossi L.; Tiezzi F.
File in questo prodotto:
File Dimensione Formato  
1-s2.0-S0164121220300716-main (1).pdf

Accesso chiuso

Dimensione 2.9 MB
Formato Adobe PDF
2.9 MB Adobe PDF   Richiedi una copia

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

Utilizza questo identificatore per citare o creare un link a questa risorsa: https://hdl.handle.net/2158/1243605
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 18
  • ???jsp.display-item.citation.isi??? 16
social impact