Specifica e verifica di sistemi critici
A.A. 2025/2026
Obiettivi formativi
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.
Risultati apprendimento attesi
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.
Periodo: Terzo quadrimestre
Modalità di valutazione: Esame
Giudizio di valutazione: voto verbalizzato in trentesimi
Corso singolo
Questo insegnamento può essere seguito come corso singolo.
Programma e organizzazione didattica
Edizione unica
Responsabile
Periodo
Terzo quadrimestre
Programma
- Introduzione: Sistemi safety e security-critical. Cosa sono ed a cosa servono i Metodi Formali. Applicazione dei Metodi Formali alla progettazione ed all'analisi di sistemi critici.
- Modellazione ed analisi ad alto livello di astrazione: Le Abstract State Machines (ASM). Tecniche di raffinamento di modelli. Il tool-set ASMETA per modelli ASM. Casi di studio di specifica di sistemi.
- Modellazione ed analisi a basso livello di astrazione. Automi di Kripke e Logica Temporale CTL: sintassi, semantica, pattern di specifica. Algoritmi di model checking. Simbolic Model Checking con rappresentazione mediante OBDD. Verifica di proprietà temporali: proprietà di raggiungibilità, di safety, di liveness, di fairness, assenza di deadlock. Raffinamenti di modelli: mappatura di modelli ad alto livello di astrazione verso modelli temporali. Tool: NuSMV e AsmetaSMV.
- Modellazione ed analisi ad alto livello di astrazione: Le Abstract State Machines (ASM). Tecniche di raffinamento di modelli. Il tool-set ASMETA per modelli ASM. Casi di studio di specifica di sistemi.
- Modellazione ed analisi a basso livello di astrazione. Automi di Kripke e Logica Temporale CTL: sintassi, semantica, pattern di specifica. Algoritmi di model checking. Simbolic Model Checking con rappresentazione mediante OBDD. Verifica di proprietà temporali: proprietà di raggiungibilità, di safety, di liveness, di fairness, assenza di deadlock. Raffinamenti di modelli: mappatura di modelli ad alto livello di astrazione verso modelli temporali. Tool: NuSMV e AsmetaSMV.
Prerequisiti
E' fortemente consigliato il superamento dell'esame di "Logica".
Metodi didattici
Lezioni frontali
Attività di laboratorio
La frequenza è fortemente consigliata.
Attività di laboratorio
La frequenza è fortemente consigliata.
Materiale di riferimento
1) Egon Boerger, Robert Staerk. Abstract State Machines. A Method for High-Level System Design and Analysis. Springer Verlag, 2003.
2) Michael Huth , Mark Ryan. Logic in Computer Science: modelling and reasoning about systems (2nd edition). Cambridge University Press, 2004.
3) B. Berard et al., System and Software Verification Model-Checking Techniques and Tools, Springer Verlag, 2001.
2) Michael Huth , Mark Ryan. Logic in Computer Science: modelling and reasoning about systems (2nd edition). Cambridge University Press, 2004.
3) B. Berard et al., System and Software Verification Model-Checking Techniques and Tools, Springer Verlag, 2001.
Modalità di verifica dell’apprendimento e criteri di valutazione
L'esame consiste di una prova scritta e in una pratica in laboratorio, entrambe obbligatorie ed entrambe della durata di due ore.
La prova scritta verte ad accertare l'acquisizione delle competenze sugli aspetti teorici dell'insegnamento; la prova pratica verte ad accertare l'acquisizione della capacità d'uso di ambienti software per la specifica, validazione e verifica di proprietà di sistemi.
Ciascuna prova è valutata in trentesimi e il voto complessivo è la media di voti riportati nelle due prove.
La prova scritta verte ad accertare l'acquisizione delle competenze sugli aspetti teorici dell'insegnamento; la prova pratica verte ad accertare l'acquisizione della capacità d'uso di ambienti software per la specifica, validazione e verifica di proprietà di sistemi.
Ciascuna prova è valutata in trentesimi e il voto complessivo è la media di voti riportati nelle due prove.
Docente/i