Davide Sangiorgi

Nella mia ricerca mi occupo di teoria della concorrenza, con particolare riguardo per i sistemi distribuiti. Cerco di sviluppare modelli e tecniche per l'analisi e la verifica di software su tali sistemi. Utilizzo per questo calcoli di processi, logiche modali e temporali, teorie di equivalenza comportamentale tra processi, sistemi di tipo. Studio i modelli anche come base per nuovi linguaggi di programmazione per sistemi concorrenti o distribuiti.

Lo sviluppo di equivalenze comportamentali (e teorie equazionali) per i calcoli di processi mobili è fondamentale in una teoria della concorrenza, dato che tali teorie costituiscono un elemento essenziale nella formalizzazione e costruzione di metodi di verifica di prorietà importanti di varia natura, quali ad esempio la sicurezza del flusso di informazione, la segretezza e l'autenticazione, nella dimostrazione di corretettezza di trasformazioni di codice, nelle tecniche di confronto di espressività di formalismi. Nel caso di sistemi distribuiti o, piu' generalmente, di linguaggi di ordine superiore (dove parti di codice o di processi possono essere copiati e/o comunicati) queste teorie sono oggi ancora poco sviluppate a causa di difficolta' tecniche ben note. Forme anche minimali di mobilità creano difficoltà sorprendenti nella modellazione di semplici equivalenze basate sulla bisimulazione e nell'individuazione di caratterizzazioni coinduttive di equivalenze contestuali. Difficoltà simili si riscontrano quando si utilizzano i tipi per disciplinare il comportamento dei processi. Mi occupo di logiche modali per sistemi distribuiti che permettono di descrivere, oltre che proprieta' comportamentali dei processi, anche proprietà topologiche dell'ambiente computazionale. Studiamo espressivita' e decidibilita' di tali logiche, cercando di capire quali siano gli operatori di base piu' utili. L'obiettivo e' poi di sviluppare modalita' di alto livello, esprimibili nella logica di base, che aiutino a definire e provare proprieta' utilizzando tecniche di dimostrazione specializzate e possibilmente tool associati. Negli ultimi anni le problematiche legate al controllo delle risorse e della mobilità , in forme diverse, sono state un tema cardine della ricerca di base nella teoria dei tipi. I tipi sono qui utilizzati per fornire delle garanzie sui comportamenti possibili dei processi. Sono attivo in questa area da molto tempo. Sistemi che abbiamo sviluppato, e su cui stiamo ancora lavorando, includono: tipi per il controllo dell'accesso a risorse; tipi per il controllo della distribuzione di risorse su un sistema, tipi per il controllo dell'interferenza tra processi, tipi per il controllo della mobilità degli agenti (dove i permessi per la mobilita' sono specificati mediante tipi), tipi che garantiscono la segretezza delle comunicazioni tra processi. Recentemente, ho iniziato ad occuparmi di applicazioni di calcoli di processi per l'elaborazione orientata ai servizi (SOC). Si tratta di un paradigma emergente per sistemi distribuiti che utilizza i servizi come singole unità di calcolo. I servizi sono entità autonome, indipendenti dalla piattaforma che possono essere descritti, individuati, e programmati ottenendo reti di applicazioni distribuite all'interno di una singola organizzazione o in grado di attraversarne i confini. Il mio lavoro in questo senso mira alla individuazione di un insieme minimo di primitive di base a partire dalle quali definire un calcolo di processi specifico per SOC; si tratta poi di studiare la definibilita' in questo ambito delle tecniche di specifica e verifica (inclusi tipi e logiche) che esistono per calcoli di processi standard. Sono infine interessato all'uso di calcoli e algebre di processi per analizzare sistemi complessi, come i sistemi biologici: definirne la semantica, e sviluppare tecniche per la loro verifica. Le algebre di processo consentono di dominare tale complessita` per due ragioni. La prima e` che` tali algebre consentono di astrarsi dalla struttura interna dei sub-sistemi. La seconda ragione sono le proprieta' di composizionalita' di tali algebre, che permettono di descrivere il comportamento di un sistema a partire dalle descrizioni dei sotto-sistemi che lo compongono.