BPMN collaboration models have acquired increasing relevance in software development since they shorten the communication gap between domain experts and IT specialists and permit clarifying the characteristics of software systems needed to provide automatic support for the activities of complex organizations. Nonetheless, the lack of effective formal verification capabilities can hinder the full adoption of the BPMN standard by IT specialists, as it prevents precisely check the satisfaction of behavioral properties, with negative impacts on the quality of the software. To address these issues, this paper proposes BProVe, a novel verification approach for BPMN collaborations. This combines both standard model checking techniques, through the MAUDE's LTL model checker, and statistical model checking techniques, through the statistical analyzer MULTIVESTA. The latter makes BProVe effective also on those scenarios suffering from the state–space explosion problem, made even more acute by the presence of asynchronous message exchanges. To support the adoption of the BProVe approach, we propose a complete web-based tool-chain that allows for BPMN modeling, verification, and result exploration. The feasibility of BProVe has been validated both on synthetically-generated models and on models retrieved from two public repositories. The performed validation highlighted the importance and complementarity of the two supported verification strategies.

A formal approach for the analysis of BPMN collaboration models / Corradini F.; Fornari F.; Polini A.; Re B.; Tiezzi F.; Vandin A.. - In: THE JOURNAL OF SYSTEMS AND SOFTWARE. - ISSN 0164-1212. - 180:(2021), p. 111007. [10.1016/j.jss.2021.111007]

A formal approach for the analysis of BPMN collaboration models

Tiezzi F.;
2021

Abstract

BPMN collaboration models have acquired increasing relevance in software development since they shorten the communication gap between domain experts and IT specialists and permit clarifying the characteristics of software systems needed to provide automatic support for the activities of complex organizations. Nonetheless, the lack of effective formal verification capabilities can hinder the full adoption of the BPMN standard by IT specialists, as it prevents precisely check the satisfaction of behavioral properties, with negative impacts on the quality of the software. To address these issues, this paper proposes BProVe, a novel verification approach for BPMN collaborations. This combines both standard model checking techniques, through the MAUDE's LTL model checker, and statistical model checking techniques, through the statistical analyzer MULTIVESTA. The latter makes BProVe effective also on those scenarios suffering from the state–space explosion problem, made even more acute by the presence of asynchronous message exchanges. To support the adoption of the BProVe approach, we propose a complete web-based tool-chain that allows for BPMN modeling, verification, and result exploration. The feasibility of BProVe has been validated both on synthetically-generated models and on models retrieved from two public repositories. The performed validation highlighted the importance and complementarity of the two supported verification strategies.
180
111007
Corradini F.; Fornari F.; Polini A.; Re B.; Tiezzi F.; Vandin A.
File in questo prodotto:
File Dimensione Formato  
1-s2.0-S0164121221001047-main (1).pdf

Accesso chiuso

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