Richiami 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 sequenziali. Algebre di processo e loro modelli come sistemi di transizione. Equivalenze comportamentali per l’astrazione e minimizzazione di sistemi e come base per prove di correttezza. Logiche Temporali e logiche modali e tecniche di verifica di proprieta' dei sistemi basate sul model checking.
L. Aceto, A. Ingolfsdottir, K.G. Larsen, J. Srba "Reactive systems" Cambridge University Press, 2007
R. Milner, Communication and Concurrency. Prentice Hall, 1989.
Obiettivi Formativi
Conoscenze:
Semantica dei linguaggi sequenziali e loro Fondamenti matematici. Modelli Operazionali di Sistemi Concorrenti e Distribuiti. Strumenti di Verifica di proprieta' di Sistemi.
Competenze acquisite
Progettazione ed Analisi di Sistemi concorrenti e distribuiti utilizzando linguaggi di programmazione e modelli avanzati anche basati sui approcci diversi.
Capacità acquisite al termine del corso:
Lo studente imparera' a comprendere la natura e semantica dei linguaggi di programmazione sequenziali e concorrenti ed a progettare e realizzare semplici sistemi concorrenti e a verificarne le proprieta' attraverso strumenti software
Metodi Didattici
Numero di ore totali del corso: 225
Numero di ore per studio personale e altre attività formative di tipo individuale: 143
Numero di ore relative alle attività in aula: 64
Numero di ore relative ad attività di laboratorio (lezioni in laboratorio): 12
Numero di ore per prove in itinere: 6
Altre Informazioni
Strumenti a supporto della didattica
UniFi E-Learning: http://e-l.unifi.it
Modalità:
Una prova scritta, una prova orale e un progetto.
Programma del corso
Contenuti del corso (programma dettagliato):
1. Introduzione alla semantica
Motivazioni, Semantica Operazionale, Semantica Denotazionale, Insiemi ed operazioni su insiemi. Relazioni e funzioni e loro proprieta'. Operazioni su relazioni e funzioni, induzione matematica, Sistemi di transizione, Grammatiche e linguaggi formali, Automi. Induzione strutturale. Sistemi di inferenza, Induzione sulle derivazioni, Induzione sulle regole, Contesti e congruenze.
2.Sintassi e denotazioni
Espressioni aritmetiche, linguaggio di una calcolatrice tascabile, Il principio di induzione strutturale, Composizionalita', Sintassi astratta, Semantica operazionale delle espressioni aritmetiche, Semantica denotazionale della calcolatrice tascabile. Semantica denotazionale delle Espressioni regolari, Semantica operazionale delle Espressioni regolari con equivalenza a tracce, Automi ed espressioni regolari, Equivalenza fra semantica operazionale e denotazionale.
3. Lambda-notazione e Semantica di semplice linguaggio imperativo
Lambda-notazione, Il principio di estensionalita', Costruttori di funzioni, Operatori di composizione, Insiemi parzialmente ordinati completi, Funzioni continue e minimo punto fisso, Esempi di funzioni sul dominio dei naturali. Il linguaggio TINY e sua semantica operazionale e denotazionale,: Semantica delle espressioni e dei comandi di TINY.
4. Operatori per Concorrenza e Nondeterminismo
Azioni esterne ed interne, Processi di base, Operatori di sequenzializzazione, Operatori di scelta non deterministica, Operatori di Composizione parallela Operatori di astrazione (Restrizione, Hiding, Relabelling), Operatori per definire comportamenti infiniti, Operatori che manipolano valori
5.Equivalenze comportamentali e preordini di raffinamento
Relazioni forti, Equivalenza basata sulle tracce, Bisimulazione forte, Equivalenze basate su testing, Preordini di raffinamento. Equivalenza basata sulle tracce deboli, Bisimulazione debole. Bisimulazione di branching, Relazioni basate su testing e sui fallimenti, Trattamento della divergenza.
6. CCS
Sintassi di CCS,
Azioni ed Operatori di CCS. Semantica operazionale di CCS, CCS con passaggio di valori. Equivalenze e preordini osservazionali per CCS, Bisimulazioni e bisimilarita' forte, Bisimulazioni, bisimilarita' e congruenza debole, Equivalenze basate su testing. Ragionamento equazionale in CCS. Assiomatizzazione della bisimilarita' forte. Assiomatizzazione bisimilarita' e congruenza debole.
7. Logiche per i Sistemi Concorrenti
Logiche e Proprieta' di Sistemi, Logiche proposizionali e loro modelli di interpretazione. Logiche modali, La logica HML, Logiche Temporali, La logica ACTL,
Formula caratteristica di un sistema. Proprieta' Infinitarie ed il mu-calcolo modale. Definizioni Ricorsive e Punto Fisso. Model Checking del mu-calcolo e di ACTL.
8. TAPAS
Utilizzo di TAPAS (A tool for the Analysis of Process Algebras) per la specifica e la verifica di proprieta' di sistemi concorrenti descritto con Process Algebra. Modellazione, analisi e verifica di alcuni algoritmi di mutua esclusione.