Business Process Modelling has acquired increasing relevance in software development. Available notations, such as BPMN, permit to describe activities of complex organisations. On the one hand, this shortens the communication gap between domain experts and IT specialists. On the other hand, this permits to clarify the characteristics of software systems introduced to provide automatic support for such activities. Nevertheless, the lack of formal semantics hinders the automatic verification of relevant properties. This paper presents a novel verification framework for BPMN 2.0, called BProVe. It is based on an operational semantics, implemented using MAUDE, devised to make the verification general and effective. A complete tool chain, based on the Eclipse modelling environment, allows for rigorous modelling and analysis of Business Processes. The approach has been validated using more than one thousand models available on a publicly accessible repository. Besides showing the performance of BProVe, this validation demonstrates its practical benefits in identifying correctness issues in real models.

BProVe: a Formal Verification Framework for Business Process Models / Corradini Flavio; Polini Andrea; FORNARI, FABRIZIO; Re Barbara; TIEZZI, Francesco; VANDIN, ANDREA. - STAMPA. - (2017), pp. 217-228. ((Intervento presentato al convegno 32nd IEEE/ACM International Conference on Automated Software Engineering - ASE 2017 tenutosi a Urbana Champaign, Illinois, USA nel October 30 - November 3, 2017 [10.1109/ASE.2017.8115635].

BProVe: a Formal Verification Framework for Business Process Models

TIEZZI, Francesco;
2017

Abstract

Business Process Modelling has acquired increasing relevance in software development. Available notations, such as BPMN, permit to describe activities of complex organisations. On the one hand, this shortens the communication gap between domain experts and IT specialists. On the other hand, this permits to clarify the characteristics of software systems introduced to provide automatic support for such activities. Nevertheless, the lack of formal semantics hinders the automatic verification of relevant properties. This paper presents a novel verification framework for BPMN 2.0, called BProVe. It is based on an operational semantics, implemented using MAUDE, devised to make the verification general and effective. A complete tool chain, based on the Eclipse modelling environment, allows for rigorous modelling and analysis of Business Processes. The approach has been validated using more than one thousand models available on a publicly accessible repository. Besides showing the performance of BProVe, this validation demonstrates its practical benefits in identifying correctness issues in real models.
International Conference on Automated Software Engineering
32nd IEEE/ACM International Conference on Automated Software Engineering - ASE 2017
Urbana Champaign, Illinois, USA
October 30 - November 3, 2017
Corradini Flavio; Polini Andrea; FORNARI, FABRIZIO; Re Barbara; TIEZZI, Francesco; VANDIN, ANDREA
File in questo prodotto:
File Dimensione Formato  
ase17main-mainp272-p-ecec75b-34274-preprint.pdf

Accesso chiuso

Dimensione 7.72 MB
Formato Adobe PDF
7.72 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/1243591
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 22
  • ???jsp.display-item.citation.isi??? 14
social impact