Investigación | Proyectos Financiados

VERIFICA DELLA CORRETTEZZA DI PROGRAMMI CONCORRENTI E DISTRIBUITI ATTRAVERSO SEQUENZIALIZZAZIONI E MODELLI AD AUTOMI.

Si propone l'investigazione di risultati teorici di base e di nuovi approcci pratici nell'ambito della verifica dei sistemi. In particolare, il progetto si articola nei due seguenti temi.(1) Complessità computazionale dei programmi concorrenti e parametrici.La creazione dinamica di thread in programmi concorrenti e distribuiti aggiunge un fattore di complessità all’analisi di questi sistemi, in quanto il numero di thread attive in una computazione non è fissato a priori (sistema parametrico). La classe di programmi risultante è molto interessante in pratica (ad esempio device drivers che interagiscono con il kernel di un sistema operativo). Si propone l’investigazione di nuovi modelli per la verifica automatica di questi programmi. In particolare, si rilasseranno alcune restrizioni considerate in letteratura e si estenderà lo studio a classi di specifiche oltre la raggiungibilità. Si studieranno anche modelli parametrici di reti di processi con comunicazione asincrona e chiamate ricorsive.I programmi concorrenti che utilizzano dei lock per l'accesso a risorse condivise costituiscono una classe interessante di programmi. Si propone lo studio del model-checking per questi programmi considerando diverse restrizioni ispirate dagli standard di programmazione concorrente correnti, come ad esempio re-entrant locks, uso dei lock in maniera contestuale e catene di lock limitate. (2) Implementazione di strumenti automatici per la verifica di programmi concorrenti, parametrici e distribuiti. Realizzare tool di verifica robusti richiede risorse notevoli. Si propone di proseguire la ricerca nell'ambito delle sequenzializzazioni di programmi a thread multiple (con stack e, a memoria condivisa o comunicazione asincrona) che ha come obiettivo il riutilizzo di tool per programmi sequenziali. Si vuole combinare in maniera efficiente questa tecnica con tool basati su SMT solvers, Horn-clause verifiers e tool di verifica basati sul testing. A seconda della classe di backend e della classe di programmi considerati verranno individuati dei parametri di analisi adeguati che da un lato limiteranno l’espressività dei modelli (ottenendo la decidibilità dei principali problemi di decisione) e dell’altra consentiranno una esplorazione sufficiente delle esecuzioni del sistema. Ad esempio, per i sistemi distribuiti, un parametro adeguato sembra essere il numero di operazioni send.Il model-checking è notoriamente efficace nell'analizzare programmi concorrenti con flussi di controllo particolarmente complessi e con numerosi interleaving possibili delle singole thread. Tuttavia, presenta dei limiti dovuti alla complessità computazione nel trattare programmi data-intensive. Si propone di investigare un approccio ibrido che combini il testing e il model-checking per ovviare alle difficoltà del model-checking nel trattare i dati e le difficoltà del testing nel coprire tutti i possibili interleaving delle computazioni delle singole thread.