RICERCA ITALIANA     

Programma di ricerca

Fondamenti Logici dei Sistemi Distribuiti e Codice Mobile

Università di riferimento

Università degli Studi di TORINO - INFORMATICA - TORINO(TO)

Responsabile dell'Unità di ricerca

Mario COPPO

Descrizione

Il programma di ricerca e' diviso secondo i task del progetto in cui è coinvolta la nostra unità



Sistemi di Tipi


Il nostro obiettivo e' quello di sviluppare e analizzare sistemi di tipi adatti a esprimere proprieta' come controllo di mobilita' e accesso a risorse in uno scenario di "global computing" dove gli agenti computazionali sono mobili e possono interagire in vari modi col contesto: consumando o offrendo risorse, scambiando dati e codice, modificando lo stato di altre componenti. In quest'ottica i tipi spesso contengono informazioni circa le azioni che possono essere svolte dai processi e i termini ben tipati possono essere visti come agenti che portano una prova certificata di (alcuni aspetti del) loro comportamento. Sebbene molto lavoro sia stato fatto in questa direzione siamo ancora lontani dall'avere una visione consolidata di cosa debbano rappresentare i tipi in questo contesto e di quali metodologie e strumenti siano utili per sfruttarne le proprieta'. Un difetto principale della maggior parte dei sistemi di tipi esistenti e' rappresentata dal fatto che tutti, in misura diversa, si basano sulla presenza di assunzioni globali che non sembrano realistiche nel nostro caso.

Siamo pero' interessati a studiare i sistemi di tipi anche in un'altra prospettiva. Le regole di type-checking possono anche essere considerate come un supporto formale per la definizione di strumenti di analisi adatti a ricavare tipi corretti per processi le cui annotazioni di tipo sono mancanti o incomplete. I tipi cosi' ricavati possono poi essere confrontati con il comportamento atteso dei processi per vedere se questo e' conforme a specifiche restrizioni su mobilita' e uso di risorse. Tuttavia non molto sembra essere stato fatto in questa direzione. Un esempio e' dato dall'algoritmo di inferenza di tipi in [CDGS03] la cui implementazione (disponibile in linea) e' presentata in [G04]. Un'analoga esperienza e' in corso per il piu' ricco sistema di [CDGP04].

Il contributo dell'unita' si sviluppera' secondo due filoni principali: Disegno di Sistemi di tipi e Inferenza di tipi e analisi statica .



Disegno di Sistemi di tipi

Un obiettivo primario della nostra unita' sara' quello di studiare sistemi di tipi adatti a esprimere proprieta' di mobilita' e accesso a risorse in cui le regole di type-checking siano essenzialmente locali e non richiedano informazioni incrociate sul comportamento di agenti che potrebbero entrare in cooperazione. Siamo infatti interessati a sistemi che siano in grado accettare nuove componenti o rilasciarle in modo sicuro, senza bisogno che le verifiche di tipo sulla compatibilita' e il buon comportamento di queste siano state precedentemente effettuate. Questo richiede che alcuni controlli circa la compatibilita' dei tipi siano realizzati al momento dell'interazione. Inoltre non si puo' assumere, come in molti approcci precedenti, che solo componenti conosciute e certificate entrino a far parte del sistema, ma bisogna considerare che anche componenti non tipate o parzialmente tipate possano venirvi incluse. Questo sembra richiedere un meccanismo per consentire alcuni controlli dinamici di tipo sugli agenti non tipati o tipati in modo non certificato. Per modellare situazioni reali inoltre dobbiamo tenere in conto che i diritti di accesso dei processi non dovrebbero essere fissati una volta per sempre ma dovrebbero essere in grado essere cambiati dinamicamente da altri agenti di controllo. Per esempio un processo che richiede una stampante puo' essere autorizzato ad accedere alla risorsa quando un processo di controllo decide che e' venuto il suo turno. Questo richiede l'introduzione di opportune primitive per modificare i tipi dinamicamente mantenendo ragionevole l'overhead dovuto ai necessari controlli.

Pensiamo di sviluppare questo programma partendo da sistemi di riferimento come il Calcolo degli Ambienti o sue varianti (per esempio [LS02], [BCS01), ma considereremo anche sistemi "piatti" come D-pi [HR03] o KLAIM [BV+03]. Il nostro obiettivo e' quello di sviluppare, se possibile, metodologie applicabili a una grande classe di sistemi e non specifiche di uno in particolare. Tuttavia il nostro approccio implica una stretta interconnessione tra il disegno dei sistemi di tipo e le sottostanti primitive di comunicazione e mobilita'. Questo potrebbe avere impatto sul calcolo sottostante suggerendo l'introduzione di nuove primitive o la modifica di alcune gia' esistenti e lo sviluppo di piu' complesse nozioni di dominio basate sul concetto di membrana [B04]. In questo programma sara' importante la collaborazione con il sito di Firenze, in cui sono gia' state affrontato tematiche simili [GP03]. In questa ottica intendiamo anche studiare in modo piu' concreto sistemi ottenuti integrando primitive e concetti di linguaggi di programmazione e la rappresentazione ed elaborazione dei dati.
Siamo interessati in particolare allo studio di sistemi che integrino la mobilita' con calcoli per oggetti e con strutture-dati rappresentate mediante linguaggi come l'XML. Il sito di Venezia, con cui si intende collaborare, ha gia' sviluppato esperienze in sistemi di questo tipo [BCS01b]


Algoritmi di inferenza e analisi statica

Un'altro obiettivo primario della nostra unita' e' quello di definire strumenti di analisi basati sull'inferenza di tipi nei sistemi sviluppati nel punto precedente o in varianti di essi. A questo scopo siamo particolarmente interessati a sviluppare sistemi che abbiano la proprieta' del "principal typing", per poter definire strumenti composizionali di analisi basati su di essi. Per ottenere cio' potrebbe essere richiesta una modifica delle regole di assegnazione, per esempio per reintrodurre una nozione di ambiente globale. Tale ambiente, utile per raccogliere informazioni circa i processi cooperanti, sarebbe tuttavia necessario solo nella fase di analisi, per esplorare in maggior dettaglio il comportamento di componenti critiche. Questo approccio e' gia' stato applicato a una variante del Calcolo degli Ambienti in [CDGS03], il cui sistema di tipi e' pero' ancora in larga misura basato su assunzioni globali. Siamo anche interessati alla possibilita' di realizzare implementazioni prototipali di questi sistemi, seguendo l'approccio di [G04]

Siccome i tipi possono essere visti come strumenti per realizzare forme di analisi statica, siamo anche interessati a studiare le relazioni tra i metodi basati sull'inferenza di tipi e altri classici metodi di analisi statica applicati al controllo delle risorse in calcoli con mobilita'. Le relazioni con l'analisi di flusso, si veda per esempio [DLB00] e [CBC02], quest'ultimo in particolare sviluppato dal sito di Venezia, sembrano particolarmente interessanti.


Equivalenze comportamentali


Non sembra chiaro fino a quale punto le usuali tecniche di prova per i processi concorrenti e mobili, basati in particolare sulla definizione di equivalenze, possano essere applicate a calcoli con tipi parziali o dinamici. Lo studio delle equivalenze e' focalizzato a fornire strumenti per provare proprieta', come leggi algebriche o trasformazioni, che possono aiutare a comprendere le proprieta' dinamiche di base degli agenti e a definire utili traduzioni. Intendiamo studiare tali proprieta' utilizzando sia le tecniche consolidate della teoria della concorrenza sia (principalmente) quelle basate sulla costruzione di filtri modelli.


Bisimulazioni e lts

Vogliamo studiare la possibilita' di applicare strumenti classici come quelli basati sulla definizione di bisimulazioni e tecniche coinduttive correlate ai sistemi sopra menzionati. A questo scopo dobbiamo individuare una nozione opportuna di osservabile, e investigare come la nozione di labelled transition system (lts) puo' essere adattata/modificata per i sistemi di nostro interesse. Questo dipende anche dal tipo di interazioni col contesto che si debbono considerare (per esempio modificazione dinamica dei tipi) e dalle altre componenti del sistema (per es. oggetti). Sara' rilevante, in questa parte del programma, la cooperazione con il sito di Bologna che possiede notevole esperienza in queste tecniche ([SW01]).


Costruzione di Filtri Modelli

Un rilevante obiettivo della nostra unita' e' quello di investigare fino a che punto la costruzione di filtri modelli puo' essere applicata per definire utili equivalenze per sistemi con mobilita' e tipi dinamici o parziali e confrontarle eventualmente con le equivalenze osservazionali definite con strumenti piu' standard. Questo potrebbe richiedere un rafforzamento e modifica della struttura dei tipi per renderli sufficientemente espressivi da caratterizzare il comportamento dei processi. Proprieta' come terminazione o deadlock potrebbero essere caratterizzabili in questo modo. I labelled ransition systems potrebbero rivelarsi utili in queste costruzioni come suggerito da esperienze precedenti [MZ04]. In generale le relazioni tra lts e filtri modelli saranno approfondite.