Formal choreographic modelling advocates a correctness-by-construction principle for the development of sound communication protocols. This principle usually hinges on syntactic or semantic restrictions to rule out models that could lead to communication glitches like message losses or deadlocks. This paper explores how these restrictions impact on the usability of formal modelling. More precisely, we benchmark the use of a formal choreographic modelling language designed to support the correctness-by-construction principle of message-passing systems. To this purpose, we consider the formal choreographic modelling of real business processes taken from the official documentation of European customs business process models. In fact, following a steadily increasing trend, the European Union started to use BPMN to support the legal provisions of the customs business process models.

On Formal Choreographic Modelling: A Case Study in EU Business Processes

Ivan Lanese;Davide Rossi;
2022

Abstract

Formal choreographic modelling advocates a correctness-by-construction principle for the development of sound communication protocols. This principle usually hinges on syntactic or semantic restrictions to rule out models that could lead to communication glitches like message losses or deadlocks. This paper explores how these restrictions impact on the usability of formal modelling. More precisely, we benchmark the use of a formal choreographic modelling language designed to support the correctness-by-construction principle of message-passing systems. To this purpose, we consider the formal choreographic modelling of real business processes taken from the official documentation of European customs business process models. In fact, following a steadily increasing trend, the European Union started to use BPMN to support the legal provisions of the customs business process models.
2022
Leveraging Applications of Formal Methods, Verification and Validation.Verification Principles - 11th International Symposium, ISoLA 2022,Rhodes, Greece, October 22-30, 2022, Proceedings, Part {I}
205
219
Alex Coto, Franco Barbanera, Ivan Lanese, Davide Rossi, Emilio Tuosto
File in questo prodotto:
File Dimensione Formato  
main.pdf

embargo fino al 17/10/2023

Tipo: Postprint
Licenza: Licenza per accesso libero gratuito
Dimensione 809.84 kB
Formato Adobe PDF
809.84 kB Adobe PDF   Visualizza/Apri   Contatta l'autore

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/11585/907472
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? ND
social impact