Il corso è idealmente suddiviso in due parti: nella prima parte
vengono studiati alcuni metodi per definire la semantica
operazionale e denotazionale di linguaggi di programmazione sequenziali; nella seconda, vengono studiati alcuni formalismi per specificare, progettare, implementare, analizzare e dimostrare proprietà di sistemi concorrenti e distribuiti.
Note, dispense e articoli forniti dal docente in formato elettronico tramite il sito del corso.
Obiettivi Formativi
Lo studente imparerà a comprendere e definire la semantica dei linguaggi di programmazione ed a progettare e realizzare semplici sistemi concorrenti.
Lo studente acquisirà le competenze necessarie a verificare la correttezza di tali sistemi, anche attraverso strumenti software di supporto, ed acquisirà le basi per l'ulteriore studio e la ricerca su teoria dei sistemi distribuiti, dei sistemi real-time e dei sistemi fault-tolerant.
Metodi Didattici
Lezioni ed esercitazioni frontali.
Altre Informazioni
Ricevimento studenti: su appuntamento (contattare il docente per telefono o e-mail)
Modalità di verifica apprendimento
L'esame consiste in un colloquio orale e nello svolgimento di
un progetto/relazione su uno degli argomenti trattati a lezione.
Programma del corso
Richiami di programmazione sequenziale e concorrente, di matematica discreta e di tecniche di prova. Automi a stati finiti e sistemi di transizione etichettati. Semantica operazionale e denotazionale dei linguaggi di programmazione. Algebre e calcoli di processo e loro modelli come sistemi di transizione. Equivalenze comportamentali come strumenti di astrazione e minimizzazione di sistemi e come base per prove di correttezza. Logiche Temporali e logiche modali e tecniche di verifica di proprietà dei sistemi basate sul model checking.