Course Details for A.Y. 2015/2016
Name:
Verifica dei Sistemi Complessi / Verification of Complex systems
Basic information
Credits:
: Master Degree in Computer Science 6 CFU (b)
Degree(s):
Master Degree in Computer Science 1st anno curriculum General
Language:
English
Course Objectives
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.
Course Content
- Scope of formal verification
- Temporal logic, Kripke structures, timed automata, hybrid automata
- Reachability, Safety, Liveness, Fairness
- Modeling of protocols, hyrid systems and control systems
- Symbolic Model Checking: SMV, HyTech. Explicit Model Checking: SPIN, Murphi
- Model-checking techniques for the automatic synthesis of controllers and plans
Assessment Methods and Criteria
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.
Textbooks
- B. Bérard et al., Systems and Software Verification , Springer. http://www.springer.com/computer/programming/book/978-3-540-41523-7
Course page updates
This course page is available (with possible updates) also for the following academic years:
To read the current information on this course, if it is still available, go to the university course catalogue .
Course information last updated on: 05 settembre 2011, 14:07