Specifica e verifica di sistemi critici

L'obiettivo dell'insegnamento è di presentare le metodologie e le tecniche per la specifica rigorosa e l'analisi formale di sistemi software critici, ossia quei sistemi il cui malfunzionamento e le cui vulnerabilità possono causare danni inaccettabili. Vengono quindi presentati i fondamenti teorici e gli strumenti per la specifica formale basata su macchine a stati astratte e la verifica formale di proprietà espresse in logica temporale.

Al termine del corso, lo studente sarà in grado di sviluppare la specifica formale di un sistema critico e di validare la specifica. Lo studente acquisirà inoltre la capacità di specificare requisiti complessi tramite il raffinamento di modelli e di garantire la correttezza e la sicurezza (safety & security) del sistema tramite model checking di proprietà espresse in logica temporale.