T2: Applicazione delle tecniche di vincoli

Problemi di scheduling.

In un problema di scheduling, una soluzione deve essere eseguita così come prevista per mantenere le qualità della soluzione. Questo è però reso a volte impossibile da ambienti dinamici dove eventi imprevisti possono velocemente invalidare la soluzione. Quindi la vita di uno schedule tende ad essere molto corta, così come le qualità ad essa associate. Per ovviare a questo problema si rende necessario studiare soluzioni robuste che sono capaci di assorbire, se non tutti, almeno parte dei possibili eventi che si possono verificare durante l'esecuzione. Tre aspetti si possono distinguere nel concetto di robustezza: la capacita' di assorbire eventi imprevisti, la capacita' di produrre rapidamente una nuova soluzione quando necessario, e la capacita' di preservare la qualita' delle soluzioni. I primi due aspetti possono essere soddisfatti adottando soluzioni temporalmente flessibili, mentre il terzo puo' essere raggiunto utilizzando metodi specifici per la generazione di soluzioni flessibili di buona qualita'. Su questa base, si vuole analizzare il concetto di flessibilta' sulle risorse in modo da estendere la struttura a vincoli che sottosta alle soluzioni temporalmente flessibili. In aggiunta, si vuole sviluppare un apparato sperimentale per validare la combinazione tra soluzioni flessibili e i metodi di riparazione. Un altro aspetto interessante da considerare sono problemi di scheduling con differenti livelli di preferenza per ogni attività. Questo richiede di introdurre nuovi metodi risolutivi. In particolare, nostro principale obiettivo e' analizzare la complessita' dell'integrazione di tecniche attuali basate su attivita' con diverse preferenze in architetture di scheduling.

Analisi di sistemi concorrenti

L'obbiettivo e' di studiare l'applicazione di tecniche di vincoli all'analisi di sistemi concorrenti con spazio degli stati infinito. In questo ambito i vincoli sono usati come modello intermedio per rappresentare problemi di analisi di diversi tipi di sistemi concorrenti. Il paradigma risultante permette quindi di realizzare un possibile trasferimento di tecnologia da sistemi con vincoli a tool per l'analisi di sistemi concorrenti. In particolare ci proponiamo di studiare: la combinazione di diversi risolutori di vincoli per poter gestire sistemi concorrenti con strutture dati eterogenee, lo sviluppo di tecniche di prova composizionali basate su vincoli, e l'applicazione dei vincoli per studiare rappresentazioni simboliche per tecniche di model checking per logiche temporali basate su teoria dei giochi, particolarmente adatte per modellare sistemi aperti e multi-agente. In tutti questi sottofiloni di ricerca utilizzeremo come casi di studio i protocolli utilizzati per i web services. Questi protocolli rappresentano infatti un'applicazione particolarmente interessante per tecniche di analisi e verifica innovative. Studieremo inoltre vantaggi e svantaggi derivanti dall'applicazione di tecniche basate sulla programmazione logica con vincoli (CLP) all'analisi, la specifica e la verifica di proprietà di sistemi concorrenti. Particolare attenzione sarà posta sullo sviluppo di metodi che usino CLP per specificare i sistemi reattivi e le loro proprieta' temporali, e la specializzazione dei programmi come meccanismo di inferenza per la verifica delle proprieta' d'interesse, combinando cosi' la generalita' degli approcci basati sulla deduzione con l'automazione degli approcci basati su astrazione.

Sicurezza

Obbiettivi cruciali dei protocolli di sicurezza sono ad esempio la confidenzialità e l'autenticazione. In letteratura questi obiettivi sono di solito formalizzati come problemi di decisione. In questa maniera è possibile solo affermare se una chiave è confidenziale oppure no, o se un soggetto si autentica con un altro oppure no. L'esperienza mostra tuttavia che la sicurezza nel mondo reale è basata su livelli di sicurezza piuttosto che su garanzie categoriche e definitive di sicurezza. Usando i vincoli soft e le preferenze, vogliamo sviluppare una nozione quantitativa degli obbiettivi di sicurezza da applicare ai protocolli piu' diffusi. Particolare attenzione sarà posta anche alla specifica e studio di politiche di autorizzazione in ambienti distribuiti attraverso l'uso dei vincoli. Pensiamo anche di sviluppare un'implementazione che sarà utile per controllare automaticamente protocolli e politiche rispetto a questa nuova nozione di sicurezza. Vogliamo infine mostrare come gli agenti possano fare inferenze sui problemi o sottoproblemi di altri agenti a partire da comunicazioni che non trasportano nessuna informazione privata in maniera esplicita. Ciò può avvenire usando dei ragionamenti basati sulla propagazione di vincoli, che riescano a velocizzare la ricerca sotto condizioni di comunicazione limitata, allo stesso tempo compromettendo la tutela della privacy. In questo contesto, la teoria della probabilità e la teoria delle possibilità saranno usate per trattare il problema dell'incertezza.

Bioinformatica

Ci occuperemo della predizione della struttura tridimensionale di una proteina data la sequenza di aminoacidi che la compongono. Si intende affrontare tale problema come problema di minimizzazione di una funzione di energia le cui variabili siano le posizioni spaziali dei centri degli aminoacidi che possono assumere valori su alcuni punti di un reticolo discreto (Face Centered Cubic lattice). Svilupperemo (in C++) un risolutore di vincoli ad hoc per vincoli su reticoli adatti a discretizzare le proteine. Il nuovo risolutore andrà a rimpiazzare il risolutore di vincoli su domini finiti del SICStus Prolog attualmente utilizzato per tale problema. Il codice verra' poi portato su macchina parallela. Si desidera anche investigare l'applicabilità del modello di ottimizzazione multiagente al problema e la sua possibile generalizzazione ad altre simulazioni biologiche. In questo contesto si desidera passare da una formalizzazione nel linguaggio Linda ad un modello basato su MPI che permetta una effettiva computazione concorrente su Cluster di PC.