Anno di corso: 1

Crediti: 8
Crediti: 8
Crediti: 8
Crediti: 3
Tipo: Lingua/Prova Finale
Crediti: 3
Tipo: Lingua/Prova Finale
Crediti: 3
Tipo: Lingua/Prova Finale
Crediti: 3
Tipo: Lingua/Prova Finale

Anno di corso: 2

Anno di corso: 3

METODI FORMALI

Scheda dell'insegnamento

Anno accademico di regolamento: 
2016/2017
Anno di corso: 
3
Anno accademico di erogazione: 
2018/2019
Tipo di attività: 
Obbligatorio a scelta
Lingua: 
Italiano
Crediti: 
8
Ciclo: 
Secondo Semestre
Ore di attivita' didattica: 
72
Prerequisiti: 

Nozioni di base di logica proposizionale. Nozioni di base di analisi matematica e di matematica discreta (come trattata nel corso di fondamenti dell'nformatica).

Moduli

Metodi di valutazione

Modalita' di verifica dell'apprendimento: 

L'esame consiste in uno scritto e in un orale.

Lo scritto consiste nello svolgimento di alcuni esercizi.

Al colloquio orale, oltre a discutere la soluzione degli esercizi dello scritto, verranno fatte domande sugli argomenti sviluppati e potrà essere discussa la soluzione di alcuni esercizi di modellazione e di verifica di proprietà svolti in laboratorio durante il corso. Il testo di tali esercizi sarà a disposizione sul sito del corso.

Valutazione: 
Voto Finale

Obiettivi formativi

Alla fine del corso lo studente sarà in grado di modellare, a diversi livelli di astrazione, sistemi concorrenti semplici ma non banali e di descriverne i requisiti per mezzo di un linguaggio logico; conoscerà le tecniche per verificarne le proprietà di comportamento; saprà usare alcuni strumenti software per il disegno e l'analisi di sistemi concorrenti.

Contenuti

Ruolo e limiti dei metodi formali nella progettazione e nell'analisi del software, particolarmente nel caso di sistemi concorrenti; tecniche per definire la semantica di programmi e sistemi concorrenti; strumenti formali per specificare sistemi concorrenti, i loro requisiti e le loro proprietà; algoritmi e strumenti software per il disegno e l'analisi di sistemi concorrenti. In particolare si introdurrà la teoria delle reti di Petri.

Programma esteso

1. Panoramica dei metodi formali nell'informatica. Sistemi e programmi concorrenti.

2. Strumenti per la modellazione di sistemi concorrenti: stemi di transizioni e altre notazioni formali.

3 Analisi di sistemi concorrenti: proprietà di liveness e di safety, logiche modali e temporali, model checking

4 Reti di Petri: fondamenti concettuali, applicazioni, varianti, tecniche di analisi.

5 Teoria dei sistemi: nozioni di base dei sistemi dinamici, cenni al modello degli automi cellulari

Bibliografia consigliata

Dispense e articoli monografici forniti dal docente.

Metodi didattici

Lezioni ed esercitazioni in aula. Esercitazioni in laboratorio.