RICERCA ITALIANA     

Controllo e certificazione dell'uso delle risorse (CONCERTO)

Università degli Studi di Torino

Abstract

In questo progetto noi intendiamo gettare le fondamenta teoriche per la definizione di strumenti di analisi (essenzialmente statici) finalizzati a garantire proprietà operazionali di programmi legate in particolare all’uso delle risorse, in modelli computazionali sia sequenziali che concorrenti. Una gestione statica dell’uso delle risorse è di importanza crescente nell’ambito della computazione mobile e distribuita. L’area di ricerca a cui ci riferiamo ha come scopo quello di associare ad un programma una certificazione, che ne garantisca particolari proprietà computazionali, in particolare la quantità di risorse (tempo e spazio, ma non solo) necessarie per la sua esecuzione. Per queste finalità ci baseremo su strumenti e tecniche derivati dalla logica, più specificamente teoria della dimostrazione, e sulla semantica, guardando in particolare alla logica lineare e al lambda calcolo. La ricerca che noi vogliamo portare avanti è essenzialmente fondazionale, e può essere idealmente suddivisa in due obiettivi principali. Noi vogliamo produrre:

1. Tecniche fondazionali per l’analisi e la verifica di proprietà operazionali di programmi;
2. Teorie computazionali che modellino l’interazione corretta con l’ambiente.

Per quanto riguarda il punto (1), saremo soprattutto interessati a studiare sistemi formali che generino programmi con complessità limitata (tempo di esecuzione e spazio usato), in contrapposizione a sistemi similari che caratterizzano >>>

Coordinatore Scientifico del Programma di Ricerca

Simonetta Ronchi Della Rocca Università degli Studi di TORINO

Obiettivo del Programma di Ricerca

La sempre maggior diffusione di sistemi di elaborazione distribuiti ha reso ancora più attuali le problematiche legate alla correttezza e alla certificazione di proprietà di programmi. In questo contesto, diventa essenziale garantire e certificare proprietà run-time per reti costituite da piccole componenti mobili con risorse computazionali limitate, che ricevono dalla rete stessa i programmi da eseguire. In particolare è importante garantire che l’esecuzione di tali programmi da una parte non richieda risorse in eccesso rispetto a quelle a disposizione del componente che li deve eseguire, dall’altra non costituisca una minaccia per la sicurezza globale del sistema. In questo progetto noi intendiamo gettare le fondamenta teoriche per la definizione di strumenti di analisi (essenzialmente statica) finalizzati a garantire proprietà operazionali di programmi legate in particolare all’uso delle risorse, in modelli computazionali sia sequenziali che concorrenti. Una gestione statica dell’uso delle risorse è di importanza crescente nell’ambito della computazione mobile e distribuita.

L’area di ricerca a cui ci riferiamo ha come scopo quello di associare ad un programma una certificazione, che ne garantisca particolari proprietà computazionali, in particolare la quantità di risorse (tempo e spazio, ma non solo) necessari per la sua esecuzione. In questo modo è possibile controllare, nella maggior parte dei casi staticamente, se il componente che si vuole usare >>>

Risultati parziali attesi

Come abbiamo già illustrato al punto 11, gli obiettivi di questo progetto sono principalmente fondazionali, e di conseguenza ci aspettiamo risultati soprattutto di tipo metodologico, da ottenere mediante il raffinamento e il miglioramento del quadro teoretico ispirato dalla logica lineare sui temi del disegno e dell’analisi delle proprietà a runtime dei programmi. In particolare, vogliamo ampliare l’applicazione delle teorie e dei sistemi di tipo per la misura e il controllo dell’uso di risorse e di sviluppare a partire da queste delle tecniche generali applicabili anche nell’ambito della programmazione concorrente, e, allo stesso tempo, sviluppare nuove teorie e modelli che permettano la specifica, il controllo e la verifica della corretta interazione con l’ambiente (ad esempio, allo scopo di caratterizzare nuove classi di complessità oppure di analizzare nuovi paradigmi computazionali). Vogliamo anche verificare l’applicabilità di alcuni dei risultati ottenuti implementando alcuni prototipi. Descriveremo prima i risultati metodologici che ci attendiamo, seguendo lo schema con cui abbiamo presentato i temi di ricerca al punto 14, “Ruolo di ciascuna unità operativa in funzione degli obiettivi previsti e relative modalità di integrazione e collaborazione”. Considereremo prima i risultati attesi nell’ambito Obiettivo uno:
Tecniche fondazionali per l’analisi e la verifica di proprietà operazionali di programmi.

* Riduzione ottimale.
- Definizione di >>>

Durata

24 mesi

Base di partenza scientifica nazionale o internazionale

In anni recenti, sono emerse due importanti novità nell’ambito dello studio della computazione. In primo luogo, sistemi logici, derivati dalla logica lineare, nei quali si puó esprimere la nozione di risorsa. In secondo luogo, nuovi paradigmi computazionali come quello biologico e quello quantistico. Inoltre, anche dentro i paradigmi tradizionali, lo studio della computazione ha seguito direzioni meno specifiche rispetto ai classici modelli computazionali. Nozione comune alla logica e alla computazione è quella di interazione, con diversi significati a seconda dei contesti.

Per ridurre la frammentazione di questa sezione, descriveremo il retroterra del progetto secondo grandi aree, ciascuna concernente diversi temi di ricerca specifici. Per mancanza di spazio, i riferimenti sono incompleti: una lista più estesa di essi si può trovare nello stato dell’arte di ciascuno dei modelli B.

1. Complessità Computazionale Implicita

La Complessità Computazionale Implicita (ICC) studia con approcci indipendenti dalle macchine teorie e applicazioni della complessità computazionale, con particolare attenzione agli approcci basati sulla logica. La maggior parte del lavoro consiste nel caratterizzare classi di complessità con sistemi logici (attraverso la corrispondenza di Curry-Howard).

In particolare la Logica Lineare Leggera di Girard (LLL), la sua versione affine (LAL) di Asperti e Roversi, e la Logica Soft (SLL) di Lafont >>>