Modellazione e analisi di sistemi
A.A. 2023/2024
Obiettivi formativi
L'obiettivo dell'insegnamento è di presentare le metodologie e le tecniche per la specifica e l'analisi formale di sistemi complessi. Vengono quindi presentati i fondamenti teorici delle metodologie di modellazione astratta (operazionale e dichiarativa) e delle tecniche di verifica formale di proprietà espresse in logica temporale.
Risultati apprendimento attesi
Al termine dell'insegnamento, lo studente dovrà essere in grado di sviluppare un modello di specifica formale per un sistema complesso. Lo studente inoltre dovrà aver acquisito una capacità di modellazione tramite raffinamento di modelli ed avere competenze su metodi e tecniche per la verifica formale di proprietà temporali.
Periodo: Secondo semestre
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
Secondo semestre
Programma
- Introduzione: Cosa sono ed a cosa servono i Metodi Formali. Applicazione dei Metodi Formali alla progettazione ed all'analisi di sistemi.
- 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. Astrazione di modelli: fusione degli stati; astrazione di variabili, riduzione di variabili, observer automata. 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. Astrazione di modelli: fusione degli stati; astrazione di variabili, riduzione di variabili, observer automata. 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.
Sito Web dell'insegnamento:
http://ericcobenemas.ariel.ctu.unimi.it/
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.
Sito Web dell'insegnamento:
http://ericcobenemas.ariel.ctu.unimi.it/
Modalità di verifica dell’apprendimento e criteri di valutazione
L'esame consiste di una prova scritta ed 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 ed il voto complessivo è la media di voti riportati nelle due prove.
Gli eventuali esami a distanza saranno svolti con l'utilizzo della piattaforma exam.net, con le modalità illustrate sul portale dell'Ateneo. Le prove avranno la medesima struttura e durata possibilmente di poco ridotta rispetto a quelle in presenza.
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 ed il voto complessivo è la media di voti riportati nelle due prove.
Gli eventuali esami a distanza saranno svolti con l'utilizzo della piattaforma exam.net, con le modalità illustrate sul portale dell'Ateneo. Le prove avranno la medesima struttura e durata possibilmente di poco ridotta rispetto a quelle in presenza.
Siti didattici
Docente/i