The BPMN 2.0 standard is a widely used semi-formal notation to model distributed information systems from different perspectives. The standard makes available a set of diagrams to represent such perspectives. Choreography diagrams represent global constraints concerning the interactions among system components without exposing their internal structure. Collaboration diagrams instead permit to depict the internal behaviour of a component, also referred as process, when integrated with others so to represent a possible implementation of the distributed system. This paper proposes a design methodology and a formal framework for checking conformance of choreographies against collaborations. In particular, the paper presents a direct formal operational semantics for both BPMN choreography and collaboration diagrams. Conformance aspects are proposed through two relations defined on top of the defined semantics. The approach benefits from the availability of a tool we have developed, named C4, that permits to experiment the theoretical framework in practical contexts. The objective here is to make the exploited formal methods transparent to system designers, thus fostering a wider adoption by practitioners.

Collaboration vs. choreography conformance in BPMN

Flavio Corradini
;
Andrea Morichetta;Andrea Polini;Barbara Re;
2020-01-01

Abstract

The BPMN 2.0 standard is a widely used semi-formal notation to model distributed information systems from different perspectives. The standard makes available a set of diagrams to represent such perspectives. Choreography diagrams represent global constraints concerning the interactions among system components without exposing their internal structure. Collaboration diagrams instead permit to depict the internal behaviour of a component, also referred as process, when integrated with others so to represent a possible implementation of the distributed system. This paper proposes a design methodology and a formal framework for checking conformance of choreographies against collaborations. In particular, the paper presents a direct formal operational semantics for both BPMN choreography and collaboration diagrams. Conformance aspects are proposed through two relations defined on top of the defined semantics. The approach benefits from the availability of a tool we have developed, named C4, that permits to experiment the theoretical framework in practical contexts. The objective here is to make the exploited formal methods transparent to system designers, thus fostering a wider adoption by practitioners.
File in questo prodotto:
File Dimensione Formato  
2002.04396v7.pdf

accesso aperto

Tipologia: Versione Editoriale
Licenza: PUBBLICO - Creative Commons
Dimensione 2.22 MB
Formato Adobe PDF
2.22 MB Adobe PDF Visualizza/Apri

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/444268
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 5
  • ???jsp.display-item.citation.isi??? 2
social impact