Verifica di Well-Formedness in un Tool per Choreography Automata

In questo elaborato viene presentato un lavoro di estensione e miglioramento di Corinne, un tool per la lettura, composizione e proiezione dei Choreography Automata. Questi sono un modello emergente basato sul concetto di automi a stati finiti impiegato principalmente per la descrizione top-down di coreografie di sistemi distribuiti. In particolare il progetto si concentra nel l’implementazione della verifica di Well-formedness, caratteristica fondamentale di un c-automaton al fine di garantirne una correttezza strutturale, priva dei tipici errori della programmazione concorrente, come Deadlocks e le Race Conditions.