In the last years we are observing a growing interest in verification of business process models that, despite their lack of formal characterisation, are widely adopted in industry and academia. To this aim, a formalization of the execution semantics of business process modelling languages is essential. In this paper, we focus on the OMG standard BPMN 2.0. Specifically, we provide a direct formalisation of its semantics in terms of Labelled Transition Systems. This approach permits to avoid possible miss-interpretations, due to the usage of the natural language in the standard specification, and to over- come issues due to the mapping of BPMN to other formal languages, which are equipped with their own semantics. Our operational semantics is given for a relevant subset of BPMN elements focusing on the capability to model collaborations among organisations via message exchange. One of its distinctive aspects is the suitability to model business processes with arbitrary topology. This allows designers to freely specify their processes according to the reality, without the limitation of defining well-structured models. The provided formalization is also implemented by exploiting the capabilities of Maude. This implementation takes a collaboration model as an input and, explores all the model executions. By relying on it, automatic verification of properties related to collaborations has been carried out via the Maude model checker. We illustrate the benefits of our approach by means of a simple, yet realistic, running example concerning a travel booking scenario.

A Formal Approach to Modelling and Verification of Business Process Collaborations

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

Abstract

In the last years we are observing a growing interest in verification of business process models that, despite their lack of formal characterisation, are widely adopted in industry and academia. To this aim, a formalization of the execution semantics of business process modelling languages is essential. In this paper, we focus on the OMG standard BPMN 2.0. Specifically, we provide a direct formalisation of its semantics in terms of Labelled Transition Systems. This approach permits to avoid possible miss-interpretations, due to the usage of the natural language in the standard specification, and to over- come issues due to the mapping of BPMN to other formal languages, which are equipped with their own semantics. Our operational semantics is given for a relevant subset of BPMN elements focusing on the capability to model collaborations among organisations via message exchange. One of its distinctive aspects is the suitability to model business processes with arbitrary topology. This allows designers to freely specify their processes according to the reality, without the limitation of defining well-structured models. The provided formalization is also implemented by exploiting the capabilities of Maude. This implementation takes a collaboration model as an input and, explores all the model executions. By relying on it, automatic verification of properties related to collaborations has been carried out via the Maude model checker. We illustrate the benefits of our approach by means of a simple, yet realistic, running example concerning a travel booking scenario.
2018
File in questo prodotto:
File Dimensione Formato  
SCP.pdf

solo gestori di archivio

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