SCHEDA DELL'INSEGNAMENTO (SI)
SSD ING-INF/05
LAUREA MAGISTRALE IN INGEGNERIA INFORMATICA
ANNO ACCADEMICO: 2022-2023
INFORMAZIONI GENERALI - DOCENTE
DOCENTE: VALERIA VITTORINI
TELEFONO: 0817683847
EMAIL: Questo indirizzo email è protetto dagli spambots. È necessario abilitare JavaScript per vederlo.
INFORMAZIONI GENERALI - ATTIVITÀ
INSEGNAMENTO INTEGRATO (EVENTUALE):
MODULO (EVENTUALE):
CANALE (EVENTUALE):
ANNO DI CORSO (I, II, III): II
SEMESTRE (I, II): II
CFU: 3
(se previsti dall'Ordinamento del CdS)
...................................................................................................................................................
EVENTUALI PREREQUISITI
...................................................................................................................................................
OBIETTIVI FORMATIVI
Obiettivo del corso di metodi formali è introdurre gli studenti conoscenze alla modellazione e verifica di sistemi software e computer-based, con particolare riferimento a tecniche di verifica formale.
Verranno illustrati il ruolo e l'importanza dei metodi formali nello sviluppo di sistemi complessi e verranno introdotti diversi strumenti formali utilizzati per la modellazione di sistemi e di proprietà. Infine verranno affrontati aspetti avanzati in particolare nell'ambito delle metodologie di modellazione di sistemi complessi.
(Descrittori di Dublino)
Conoscenza e capacità di comprensione
Lo studente deve dimostrare di conoscere e comprendere il ruolo dei modelli formali per l’analisi di sistemi critici, e in particolare per la verifica di proprietà e per la validazione.
Capacità di applicare conoscenza e comprensione
Lo studente deve dimostrare di saper sviluppare e analizzare semplici modelli espressi mediante i formalismi presentati durante il corso.
PROGRAMMA-SYLLABUS
Parte I: Il ruolo dei metodi formali nell'ingegneria dei sistemi, i metodi formali nella certificazione dei sistemi reali, alcuni esempi tratti dal mondo reale, proprietà funzionali e non funzionali, analisi qualitativa e quantitativa. Petri nets ed estensioni tempificate per l’analisi quantitativa di proprietà temporali.
Parte II: linguaggi formali per la specifica e l'analisi. Logiche temporali, LTL e CTL, introduzione al model checking. tecniche di sviluppo di modelli complessi, strumenti per la modellazione e la risoluzione dei modelli.
Parte III: esercitazioni e applicazione a casi di studio.
MATERIALE DIDATTICO
Appunti del corso, articoli scientifici.
MODALITÀ DI SVOLGIMENTO DELL'INSEGNAMENTO
Lezioni frontali (50%), esercizi e attività di laboratorio (40%), seminari applicativi (10%).
VERIFICA DI APPRENDIMENTO E CRITERI DI VALUTAZIONE
a) Modalità di esame:
| L'esame si articola in prova: | |
| Scritta e orale | |
| Solo scritta o intercorso a metà | |
| Solo orale | |
| Discussione di elaborato progettuale |  |
| Altro | |
| In caso di prova scritta i quesiti sono (*): | |
| A risposta multipla | |
| A risposta libera | |
| Esercizi numerici | |