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. - In: SCIENCE OF COMPUTER PROGRAMMING. - ISSN 0167-6423. - STAMPA. - 166:(2018), pp. 35-70. [10.1016/j.scico.2018.05.008]

A Formal Approach to Modelling and Verification of Business Process Collaborations

Francesco Tiezzi
2018

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.
166
35
70
Flavio Corradini; Fabrizio Fornari; Andrea Polini; Barbara Re; Francesco Tiezzi
File in questo prodotto:
File Dimensione Formato  
SCP.pdf

Accesso chiuso

Dimensione 1.73 MB
Formato Adobe PDF
1.73 MB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in FLORE 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/2158/1243611
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 32
  • ???jsp.display-item.citation.isi??? 25
social impact