Studiare

In questa sezione è possibile reperire le informazioni riguardanti l'organizzazione pratica del corso, lo svolgimento delle attività didattiche, le opportunità formative e i contatti utili durante tutto il percorso di studi, fino al conseguimento del titolo finale.

Piano Didattico

A.A. 2024/2025 A.A. 2023/2024 A.A. 2022/2023 A.A. 2021/2022 A.A. 2020/2021 A.A. 2019/2020 A.A. 2018/2019 A.A. 2017/2018 A.A. 2016/2017 A.A. 2015/2016 A.A. 2014/2015 A.A. 2013/2014 A.A. 2012/2013 A.A. 2011/2012 A.A. 2010/2011 A.A. 2009/2010

Queste informazioni sono destinate esclusivamente agli studenti e alle studentesse già iscritti a questo corso.
Se sei un nuovo studente interessato all'immatricolazione, trovi le informazioni sul percorso di studi alla pagina del corso:

Laurea magistrale in Ingegneria e scienze informatiche - Immatricolazione dal 2025/2026

Il piano didattico è l'elenco degli insegnamenti e delle altre attività formative che devono essere sostenute nel corso della propria carriera universitaria.
Selezionare il piano didattico in base all'anno accademico di iscrizione.

CURRICULUM TIPO:

1° Anno 

InsegnamentiCreditiTAFSSD
12
B
ING-INF/05
6
B
ING-INF/05
12
B
INF/01
12
B
ING-INF/05
6
C
INF/01
6
B
ING-INF/05
6
B
ING-INF/05

2° Anno   Attivato nell'A.A. 2016/2017

InsegnamentiCreditiTAFSSD
6
B
INF/01
6
B
ING-INF/05
Altre attivita' formative (taf f)
4
F
-
24
E
-
InsegnamentiCreditiTAFSSD
12
B
ING-INF/05
6
B
ING-INF/05
12
B
INF/01
12
B
ING-INF/05
6
C
INF/01
6
B
ING-INF/05
6
B
ING-INF/05
Attivato nell'A.A. 2016/2017
InsegnamentiCreditiTAFSSD
6
B
INF/01
6
B
ING-INF/05
Altre attivita' formative (taf f)
4
F
-
24
E
-
Insegnamenti Crediti TAF SSD
Tra gli anni: 1°- 2°
Due insegnamenti a scelta
6
C
INF/01
6
C
INF/01
6
C
FIS/01
6
C
INF/01
6
C
INF/01
6
C
SECS-P/10
6
C
INF/01
6
C
INF/01
6
C
INF/01
6
C
INF/01
Tra gli anni: 1°- 2°
8
D
-

Legenda | Tipo Attività Formativa (TAF)

TAF (Tipologia Attività Formativa) Tutti gli insegnamenti e le attività sono classificate in diversi tipi di attività formativa, indicati da una lettera.

A Attività di base
B Attività caratterizzanti
C Attività formative affini o integrative
D Attività a scelta dello studente
E Prova finale
F Altre attività formative
S Stage e tirocini presso imprese, enti pubblici o privati, ordini professionali

Verifica automatica di sistemi  (2015/2016)

Codice insegnamento

4S003252

Docenti

Nicola Fausto Spoto, Alessandro Cimatti

Coordinatore

Nicola Fausto Spoto

Crediti

6

Lingua di erogazione

Italiano

Settore Scientifico Disciplinare (SSD)

INF/01 - INFORMATICA

Periodo

II semestre dal 1 mar 2016 al 10 giu 2016.

Sede

VERONA

Seminari 0

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

Le/gli studentesse/studenti con disabilità o disturbi specifici di apprendimento (DSA), che intendano richiedere l'adattamento della prova d'esame, devono seguire le indicazioni riportate QUI

Materiale e documenti