Ricerca | Metodi Formali per la Verifica e la Sintesi di Sistemi

Realizzare sistemi digitali non è mai stato un compito facile ed oggi è divenuto ancor più difficile a causa della loro notevole complessità. In questo ambito, sono rilevanti le metodologie per sintetizzare automaticamente sistemi corretti nel senso che soddisfano le specifiche date (sintesi), e per verificare automaticamente il loro soddisfacimento (verifica). Sono state sviluppate diverse metodologie che in molti casi hanno prodotto applicazioni di successo a livello industriale. In particolare, le tecniche sviluppate all'interno di robuste teorie matematiche consentono di attingere a una serie di risultati e strumenti che facilitano sia la progettazione che la validazione dei tool di verifica e sintesi stessi. Un ulteriore aspetto positivo di queste metodologie è che esse non necessitano del sistema concreto per operare e solitamente sono utilizzate su un modello astratto dello stesso, e quindi in anticipo rispetto a tecniche tradizionali quali ad esempio il testing e la simulazione.

Le competenze del gruppo di ricerca in Verifica e Sintesi automatica del DI ricoprono sia aspetti teorici che pratici del model-checking per diverse classi di sistemi digitali. In particolare, sono stati studiati fondamenti teorici e sviluppate e implementate tecniche per la verifica e la sintesi di programmi sequenziali e concorrenti, sistemi real-time e ibridi con e senza costanti parametriche, sistemi aperti e modulari. Il model-checking oltre ad offrire i vantaggi dei metodi formali elencati sopra, è completamente automatico e in caso il sistema non soddisfi la specifica (bug detection), genera un controesempio che permette ai progettisti di individuare rapidamente l’errore.

Temi di ricerca

• Model-checking
• Verifica di programmi concorrenti
• Verifica di sistemi embedded
• Verifica di sistemi real-time e ibridi
• Verifica multicore
• Bounded model checking
• Generazione automatica di test cases
• Teoria degli automi
• Logica temporale
• Giochi su grafi
• Complessità computazionale
• Modelli di sistemi concorrenti

Attività Didattica

L’impegno didattico del gruppo è concentrato principalmente sui corsi di Programmazione 2 e Metodi Matematici per L’Informatica alla Laurea Triennale, e di Tecniche Automatiche per la Correttezza del Software (TACS) e Automi Linguaggi e Complessità alla Laurea Magistrale.

Strutture dell'area

Laboratorio di Verifica Automatica di Sistemi Digitali.

Collaborazioni

University of Southampton (UK), University of Pennsylvania (USA), Univeristy of Illinois at Urbana-Champaign (USA), Université de Bordeaux (France), Università di Napoli, Università di Udine, Università di Verona, ISTC-CNR Roma, Ericsson Pagani, Citel group.

Ex membri

Ilaria De Crescenzo, Dario Della Monica, Barbara Di Giampaolo, Marco Faella, Alessandro Ferrante, Maurizio Memoli, Aniello Murano, Domenico Parente, Gennaro Parlato.