A choreographic approach to modelling and analysis of administrative procedures in healthcare management

Choreographic models in general, and Choreographic Automata (CA)and global choreographies (g-choreography) in particular, can be used to analyse and validate communicating systems. This thesis applied these models to a case study in healthcare management, the procedure for accreditation and authorisation of public and private healthcare structures in the Emilia Romagna region (Italy). In this thesis, we verified the realisability of communicating systems using CA and g-choreography in general, and of the case study in particular. We first formalised the case study using a BPMN collaboration diagram based on the natural-language description. Initially, we converted the BPMN model into CAs. Afterward, we verify the correctness of the system using the Corinne tool, as its underlying theory is CAs. The tool Corinne showed a few issues in the formalised model, but it turned out that such issues were due to too strict requirements posed by the theory underlying Corinne. This gave us useful feedback for future improvements of Corinne and its underlying theory. Due to some limitations in the CA and Corinne such as the explosion of the size of the model due to the fact that CAs model concurrency by explicitly representing all the interleavings, we moved to g-choreographies to enable the analysis of the correctness of its communication patterns using the PomCho tool. This requires to refine PomCho and its underlying theoretical framework. First, we extend PomCho to support not only asynchronous communication, but also synchronous one. Moreover, in both cases, we provide a more efficient algorithm to check closure properties ensuring realisability of choreographies. We refer to the extended version of PomCho as PomCho+. The new algorithm allows us to check realisability of larger pomsets than before, which makes our approach viable for complex systems such as our case study.