Dettagli sull'Insegnamento per l'A.A. 2013/2014

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.

Risorse Internet

Aggiornamenti alla pagina del corso

• A.A. 2010/2011
• A.A. 2013/2014
• A.A. 2014/2015
• A.A. 2015/2016
• A.A. 2016/2017
• A.A. 2017/2018
• A.A. 2018/2019