Modelli e metodi per la verifica composizionale (PRIN 2006)

Data inizio
9 febbraio 2007
Durata (mesi) 
24
Dipartimenti
Informatica
Responsabili (o referenti locali)
Segala Roberto

La verifica formale si riferisce al processo di specifica e dimostrazione rigorosa delle proprietà che devono essere soddisfatte da un sistema. E' usata in maniera estensiva per scoprire celermente errori durante le varie fasi di progettazione ed implementazione di un sistema, specialmente in applicazioni safety-critical (es., controllo di traffico aereo, strumentazione medica, processi industriali), e in applicazioni in cui gli errori comportano costi elevati (es., microprocessori, esploratori spaziali). L'obiettivo iniziale di questo progetto è di mobilitare, unire e rafforzare i gruppi di ricerca che vi partecipano attraverso un obiettivo comune, cioè la progettazione di un sistema integrato di verifica automatica e semi-automatica. Sebbene ci sia una generale preferenza nei confronti di tool completamente automatici, la continua crescita in complessità dei dispositivi moderni richiede un buon bilanciamento tra intervento umano e verifica totalmente automatica.

Siamo particolarmente interessati alla verifica di sistemi reattivi complessi che contengano aspetti real-time, stati potenzialmente infiniti, descrizioni parametriche, comportamento stocastico, e comportamento ibrido. L'obiettivo di un sistema di verifica integrato costituisce un'ossatura comune e un elemento guida ideale per l'estensione ibrida e stocastica dei modelli correnti, la progettazione di nuove tecniche per la decomposizione di problemi complessi in problemi semplici e trattabili, la progettazione di algoritmi di verifica più potenti (es., real-time bounded model checking, ragionamento ibrido approssimato), e il miglioramento dei tool correntemente sviluppati in Italia (es., CMurphi, NuSMV, Ariadne).

Potenziali campi di applicazione da usare come casi di studio sono i sistemi distribuiti, i protocolli crittografici e probabilistici, i sistemi embedded, e i sistemi e programmi multithread.

Enti finanziatori:

PRIN VALUTATO POSITIVAMENTE
Finanziamento: richiesto
Programma: COFIN - Progetti di Ricerca di Interesse Nazionale

Partecipanti al progetto

Augusto Parma
Roberto Segala
Professore ordinario
Nicola Fausto Spoto
Professore associato
Andrea Turrini

Collaboratori esterni

Ruggero Lanotte
Insubria

Attività

Strutture