Modellazione e analisi di sistemi
A.A. 2018/2019
Obiettivi formativi
Il corso presenta metodologie e tecniche per la specifica e l'analisi formale di sistemi complessi. Lo studente imparerà i fondamenti teorici delle metodologie di modellazione astratta sia di tipo operazionale che dichiarativo, e delle tecniche di validazione e verifica formale basate su simulazione, testing, e model checking. Alla fine del corso lo studente sarà in grado di usare specifici linguaggi di specifica che consentono di descrivere un sistema da analizzare e le proprietà da provare, nonché gli strumenti automatici (tool) che permettono la verifica ((semi-)automatica e/o interattiva) delle proprietà di un sistema.
Risultati apprendimento attesi
Capacità di sviluppo di un modello di specifica formale per un sistema complesso. Capacità di modellazione tramite raffinamento di modelli. 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 non può essere seguito come corso singolo. Puoi trovare gli insegnamenti disponibili consultando il catalogo corsi singoli.
Programma e organizzazione didattica
Edizione unica
Responsabile
Periodo
Secondo semestre
STUDENTI FREQUENTANTI
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. Tecniche di astrazione. 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. Tecniche di astrazione. 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.
Informazioni sul programma
Capacità di sviluppo di un modello di specifica formale per un sistema complesso. Capacità di modellazione tramite raffinamento di modelli. Competenze su metodi e tecniche per la verifica formale di proprietà temporali.
Propedeuticità
Linguaggi di Programmazione per la Sicurezza, Logica.
Prerequisiti
Concetti di informatica di base e quelli forniti nei corsi di "Progettazione/Ingegneria del Software" e di "Logica".
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 del corso; 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.
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 del corso; 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.
Metodi didattici
Lezioni frontali
Materiale di riferimento
STUDENTI NON FREQUENTANTI
· Egon Boerger, Robert Staerk. Abstract State Machines. A Method for High-Level System Design and Analysis. Springer Verlag, 2003.
· Michael Huth , Mark Ryan. Logic in Computer Science: modelling and reasoning about systems (2nd edition). Cambridge University Press, 2004.
· B. Berard et al., System and Software Verification Model-Checking Techniques and Tools, Springer Verlag, 2001.
· Michael Huth , Mark Ryan. Logic in Computer Science: modelling and reasoning about systems (2nd edition). Cambridge University Press, 2004.
· B. Berard et al., System and Software Verification Model-Checking Techniques and Tools, Springer Verlag, 2001.
Prerequisiti
Sono prerequisiti le conoscenze acquisite nel corso di Logica.
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 del corso; 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.
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 del corso; 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.
Docente/i