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


Statistiche per i requisiti di trasparenza (Attuazione Art. 2 del D.M. 31/10/2007, n. 544)

Statistiche esiti
Esiti Esami Esiti Percentuali Media voti Deviazione Standard
Positivi 82.75% 29 1
Respinti --
Assenti 17.24%
Ritirati --
Annullati --
Distribuzione degli esiti positivi
18 19 20 21 22 23 24 25 26 27 28 29 30 30 e Lode
0.0% 0.0% 0.0% 0.0% 0.0% 0.0% 0.0% 0.0% 12.5% 12.5% 8.3% 0.0% 25.0% 41.6%

Valori relativi all'AA 2015/2016 calcolati su un totale di 29 iscritti. I valori in percentuale sono arrotondati al numero intero più vicino.