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

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 

2° Anno   Attivato nell'A.A. 2022/2023

InsegnamentiCreditiTAFSSD
Prova finale
24
E
-
Attivato nell'A.A. 2022/2023
InsegnamentiCreditiTAFSSD
Prova finale
24
E
-
Insegnamenti Crediti TAF SSD
Tra gli anni: 1°- 2°
Tra gli anni: 1°- 2°
Altre attività
3
F
-
Tra gli anni: 1°- 2°

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.




S Stage e tirocini presso imprese, enti pubblici o privati, ordini professionali

Codice insegnamento

4S003252

Coordinatore

Matteo Cristani

Crediti

6

Lingua di erogazione

Italiano

Settore Scientifico Disciplinare (SSD)

INF/01 - INFORMATICA

Periodo

Primo semestre dal 4 ott 2021 al 28 gen 2022.

Obiettivi formativi

Il corso si propone di fornire i concetti fondamentali di verifica di sistemi sia hardware che software, per esempio usando logiche temporali e semantica delle tracce per rappresentarne il comportamento. Al termine del corso lo studente (1) avrà acquisito le conoscenze tecniche della verifica basata su modelli, (2) saprà utilizzarle per modellare il comportamento di specifici sistemi sia hardware che software e (3) sarà in grado di proseguire, anche autonomamente, lo studio e la ricerca nell’ambito delle tecnologie per la verifica formale di sistemi.

Programma

Verifica dei sistemi:
l’approccio basato sul model checking
Sistemi di modellazione concorrenti:
sistemi di transizione,
parallelismo e comunicazione,
esplosione degli stati
Proprietà del tempo lineare:
safety e invarianti,
liveness,
fairness
Linear Temporal Logic:
sintassi,
semantica,
model checking in LTL
Computation Tree Logic:
sintassi,
semantica,
espressività di CTL vs LTL,
model checking simbolico
CTL *
Equivalenza e astrazione:
bisimulazione,
bisimulazione e equivalenza in CTL *

Modalità d'esame

L’esame consiste in una prova scritta, ed in un orale integrativo, cui lo studente è ammesso, su propria richiesta, al superamento della prova scritta con una votazione di almeno 24/30. Se lo studente non richiede la prova orale integrativa, il voto dello scritto è definitivo.

La prova scritta verterà sugli argomenti del corso, e sarà articolata in due parti.
La parte teorica della prova, a valere per il 50% del voto, richiederà la conoscenza degli argomenti trattati a lezione, con una domanda per ciascuno dei macro-argomenti: Sistemi di modellazione concorrenti, Proprietà del tempo lineare, Linear Temporal Logic, Computation Tree Logic, CTL*, Equivalenza e astrazione.
La parte applicata della prova, a valere per il residuo 50%, richiederà la verifica delle competenze acquisite specificamente su Sistemi di transizione, Model checking su logiche temporali, Bisimulazione, Astrazione.

La prima parte della prova orale consisterà in domande relative agli stessi contenuti teorici del corso trattati nella prova scritta, e la seconda parte consisterà nello svolgimento de visu di un esercizio selezionato dal docente sugli stessi argomenti della prova scritta.

La valutazione della prova scritta terrà conto di:

- ampiezza della conoscenza di sistemi a transizione, logiche temporali, modelli di astrazione;
- correttezza dello svolgimento degli esercizi;
- completezza della conoscenza degli argomenti trattati.

La valutazione della prova orale terrà conto di:

- completezza analitica nella risposta ai quesiti;
- competenza sui temi specificati nel programma;
- correttezza delle risposte, e loro ampiezza.

La modalità a distanza è comunque garantita per tutti gli studenti che lo chiederanno nell’anno accademico 2020/21

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