Choreographic Automata: A Case Study in Healthcare Management

Choreographic models in general, and Choreographic Automata (CA) in particular, can be used to analyze and validate communicating systems. We applied CAs to a case study in healthcare management, the procedure for accreditation and authorization of public and private healthcare structures in the Emilia Romagna region (Italy). We formalized the procedure first using a BPMN collaboration diagram as intermediate step, and then using CAs. The tool Corinne showed a few issues in the formalized 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.