Automated Software Verification
Insegnamento: Automated Software Verification
Titolo insegnamento in inglese: Automated Software Verification
Lingua: italiano
Anno di corso: 2
Semestre: 2
CFU: 6
Insegnamenti propedeutici previsti: Nessuno.
Docenti:
- Massimo Benerecetti
Obiettivi Formativi
Il corso si propone di fornire le nozioni di base sottostanti il problema della verifica automatica di proprietà di correttezza di sistemi informatici software e hardware. In particolare, verranno introdotte e studiate le tecniche di Model Checking. I principali obiettivi del corso sono quelli di familiarizzare lo studente con gli strumenti fondamentali per la comprensione e l'utilizzo degli strumenti automatici di verifica, lo studio dei principali algoritmi di verifica automatica, alcune delle più importanti ottimizzazioni ed estensioni delle tecniche di Model Checking in uso nelle realtà produttive coinvolte nello sviluppo di sistemi sia hardware che software, sistemi embedded (ad es., sistemi automotive e internet-of-things) e sistemi safety-critical (ad es., sistemi di controllo di traffico ferroviario e aereo).
Programma
La parte iniziale del corso riguarderà lo sviluppo dei prerequisiti relativi agli strumenti di base per la modellazione di sistemi software e hardware e delle loro proprietà di correttezza. In questa fase, verranno richiamati elementi di logica classica e logica modale; automi a stati finiti su parole finite e su parole infinite; tecniche di base e linguaggi per la modellazione di sistemi software e hardware tramite sistemi a transizione e macchine a stati. Verranno inoltre descritti e studiati linguaggi per la specifica di proprietà di correttezza, nello specifico logiche temporali lineari (LTL) e ramificate (CTL). In seguito, verranno descritte le tecniche algoritmiche per la soluzione automatica dei problemi di verifica: Model Checking esplicito per proprietà CTL; Model Checking per proprietà LTL basato su automi; il problema dell'esplosione del spazio degli stati e il Model Checking simbolico basato su OBDD. Durante il corso verranno, inoltre, impiegati tool di model checking (NuSMV e SPIN) con esempi di utilizzo.
Modalità didattiche
Lezioni frontali.
Materiale didattico
E. M. Clarke, O. Grumberg D. Peled: "Model Checking". Lucidi utilizzati per le lezioni frontali del corso
Modalità di esame
L'esame si articola in prova solo orale (es: sviluppo progetti, prova al calcolatore ...) .