Modelli e metodi per la verifica composizionale (PRIN 2006)

Starting date
February 9, 2007
Duration (months)
24
Departments
Computer Science
Managers or local contacts
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.

Sponsors:

PRIN VALUTATO POSITIVAMENTE
Funds: requested
Syllabus: COFIN - Progetti di Ricerca di Interesse Nazionale

Project participants

Augusto Parma
Roberto Segala
Full Professor
Nicola Fausto Spoto
Associate Professor
Andrea Turrini

Collaboratori esterni

Ruggero Lanotte
Insubria

Activities

Research facilities

Share