Verifica automatica di sistemi (2015/2016)

Codice insegnamento
4S003252
Docenti
Nicola Fausto Spoto, Alessandro Cimatti
Coordinatore
Nicola Fausto Spoto
crediti
6
Settore disciplinare
INF/01 - INFORMATICA
Lingua di erogazione
Italiano
Periodo
II semestre dal 1-mar-2016 al 10-giu-2016.

Orario lezioni

II semestre
Giorno Ora Tipo Luogo Note
lunedì 14.30 - 17.30 lezione Aula I  
martedì 14.30 - 16.30 lezione Laboratorio didattico Laboratorio Ciberfisico dal 15-mar-2016  al 10-giu-2016
martedì 16.30 - 18.30 lezione Aula I  

Obiettivi formativi

Il corso presenta le problematiche legate alla verifica dei sistemi complessi e le relative tecniche.

Programma

Il corso introduce il problema della modellazione dei sistemi complessi ed altamente critici, quali sistemi ferroviari, avionici, spaziali e di controllo di progetto, e dei relativi requisiti. Si presentano i sistemi a transizioni e la loro rappresentazione simbolica in forma di logica proposizionale. Si presentano le logiche temporali: Computation Tree Logic, Linear Temporal Logic, CTL*. Si descrivono gli algoritmi di verifica per model checking di CTL e la generalizzazione a sistemi a transizioni con vincoli di fairness. Si presenta la riduzione da model checking di LTL a model checking per CTL con vincoli di fairness. Si presentano gli algoritmi simbolici per il model checking basati su Binary Decision Diagrams (BDD), ed algoritmi basati su soddisfacibilità proposizionale (SAT). Si descrivono aspetti di reliability e analisi di sistemi a Triple Modular Redundancy (TMR), nozioni di Fault Tree Analysis, ed algoritmi di calcolo dei cut set e di minimizzazione. Si presentano le nozioni di astrazione, raffinamento e predicate abstraction. Si descrivono sistemi temporizzati e sistemi ibridi, con relativi risultati di decidibilità. ll corso è complementato da esercitazioni con un package per BDD e con il model checker NuSMV.

Modalità d'esame

Esame orale o progetto

Materiale didattico

Documenti

Opinione studenti frequentanti - 2015/2016