Dettagli sull'Insegnamento per l'A.A. 2013/2014
Nome:
Verifica dei Sistemi Complessi / Verification of Complex systems
Informazioni
Crediti:
: Laurea Magistrale in Informatica 6 CFU (b)
Erogazione:
Laurea Magistrale in Informatica 1° anno curriculum Generale
Lingua:
Inglese
Obiettivi
Il corso si propone di fornire una preparazione sulle tecniche di verifica formale, sia da un punto di vista teorico che pratico. Nella prima parte del corso verranno illustrati diversi strumenti formali utilizzati per la modellazione di sistemi e di proprietà. Nella seconda parte verrà approfondita l'applicazione pratica di tali strumenti formali attraverso l'utilizzo di diversi model checkers per la validazione di casi di studio reali. Infine verranno affrontati aspetti avanzati in particolare nell'ambito della sintesi automatica di sistemi reattivi.
Sillabo
- Obiettivi e utilizzo di metodi formali per la verifica di sistemi reali
- Logiche temporali, strutture di Kripke, timed automata, hybrid automata
- Proprietà di Reachability, Safety, Liveness, Fairness
- Modellazione (protocolli, sistemi ibridi, sistemi di controllo)
- Model Checking Simbolico: SMV, HyTech. Model Checking Esplicito: SPIN, Murphi
- Aspetti avanzati: uso del Model Checking per la sintesi di sistemi di controllo e pianificatori
Testi di riferimento
- B. Bérard et al., Systems and Software Verification , Springer. http://www.springer.com/computer/programming/book/978-3-540-41523-7
Modalità d'esame
La prova di esame consiste in una prova progettuale, una prova scritta sulle due parti del corso e una prova orale sulle due parti del corso.
Aggiornamenti alla pagina del corso
Le informazioni sulle editioni passate di questo corso sono disponibili per i seguenti anni accademici:
Per leggere le informazioni correnti sul corso, se ancora erogato, consulta il catalogo corsi di ateneo.
Ultimo aggiornamento delle informazioni sul corso: 05 settembre 2011, 14:07