Choreia: A Static Analyzer to Generate Choreography Automata from Go Source Code

Le coreografie sono un paradigma emergente per la descrizione dei sistemi concorrenti che sta prendendo piede negli ultimi anni. Lo scopo principale è quello di fornire al programmatore uno strumento che permetta di capire in maniera immediata il comportamento dei partecipanti all'interno del sistema e come questi interagiscono tra loro. Partendo dai singoli partecipanti, e le loro viste locali, è possibile ricomporre in maniera bottom-up l'intera coreografia (o vista globale) del sistema. Un ulteriore vantaggio delle coreografie è che, quando rispettano alcune proprietà definite, danno garanzie sull'assenza di tipici problemi di concorrenza quali Deadlocks, Liveness e Race Conditions. Esistono vari modelli formali di coreografie, questa tesi tratta nello specifico i Choreography Automata, basati su Finite State Automata (FSA). In questa tesi viene presentato Choreia: un tool di analisi statica che, partendo da un codice sorgente Go, ricava il Choreography Automaton del sistema concorrente in maniera bottom-up.tool di analisi statica che, partendo da un codice sorgente Go, ricava il Choreography Automaton del sistema concorrente in maniera bottom-up.