Metodi Formali per la Concorrenza
(Ovvero, tutto ciò che volete sapere sui sistemi distribuiti e non avete mai osato dimostrare)
Laurea in Informatica - Università di Padova
Anno Accademico 2009/2010
Obiettivi del corso
Il corso si propone di illustrare vari modelli e strumenti proposti in
letteratura per la descrizione formale di sistemi concorrenti e
distribuiti e per la verifica di proprietà di tali sistemi. Il
corso non si focalizzerà solo sulle basi teoriche ma discuterà
anche l'uso di alcuni tool come il "Edinburgh Concurrency Workbench".
Il corso dà luogo al conseguimento di 6 CFU.
Programma di massima del corso
Il corso, della durata di 48 ore, svilupperà i seguenti temi:
- Introduzione alla concorrenza e mobilità: dagli automi ai sistemi
reattivi e concorrenti.
- Il "calculus of communicating systems" (CCS), un calcolo minimale per la descrizione di sistemi concorrenti
- Equivalenza di processi: Sistemi di transizione e bisimulazione
- Proprietà dei processi: La logica di Hennessy-Milner e strumenti per la verifica
- Dal CCS ai calcoli per sistemi con mobilità (pi-calcolo, calcolo degli ambienti, ecc.) e per i web-services.
- L'uso dei tipi per ragionare sui sistemi distribuiti
Altri possibili approfondimenti riguardano:
- Calcoli per protocolli crittografici
- Modellazione di ad-hoc networks/reti di sensori
- System biology
- Reti di Petri e sistemi di riscrittura su grafi. Semantiche
concorrenti e tecniche di analisi. Applicazione alla modellazione
di workflows.
Orario del corso
Il corso fa parte del Corso di Laurea Specialistica in Informatica,
Università di Padova, ed è collocato nel II trimestre
dell'Anno Accademico 2009/10,
con inizio il 11.01.2010 e termine
il 12.03.2010, con il seguente orario (modifiche all'orario potranno
poi essere concordate con i partecipanti al corso):
Giorno |
Orario |
Aula |
Lunedì |
9.30 - 11.30 |
1BC/45 |
Martedì |
9.30 - 11.30 |
1BC/45 |
Venerdì |
9.30 - 11.30 |
1BC/45 |
Diario del corso
Indicazione dei temi discussi durante le lezioni e degli esercizi
svolti in classe e assegnati per casa (la numerazione si riferisce al
testo adottato).
- Introduzione e note storiche
- CCS: Introduzione informale
-
CCS: definizione formale (con Esercizi 2.1, 2.2, 2.3).
Esercizi: 2.7, 2.8, 2.9, 2.10 per casa
-
Discussione degli esercizi per casa.
Esercizio 2.11.
Esercizio:
Terminazione del CCS finito (senza il costrutto di costante).
Value passing CCS. Esercizio 2.12
(Per casa: contatore con CCS value passing, corrispondenza tra CCS
e CCS value passing)
-
Equivalenze comportamentali: proprietà desiderate
Equivalenze comportamentali: alcune equivalenze non completamente
soddisfacenti (iso di LTS, tracce, tracce complete).
Bisimulazione. La bisimilarita` forte ~.
(Esercizi per casa: 3.3, 3.4, 3.5).
- Discussione esercizi
- Proprietà della bisimilarità forte (massima
bisimulazione, equivalenza). String bisimulation (Es. 3.9).
Esercizio 3.11 (Proprietà del parallelo) e Esercizio 3.12.
Esercizi per casa:
String bisimulation (Es. 3.9).
Relazione tra tracce (complete) e bisimilarita` (Es. 3.11).
La bisimilarità forte è una congruenza.
-
Formalizzazione della bisimulazione come gioco.
Esercizi per casa: Es. 3.15. Bisimulazione up-to.
- Altre equivalenze: simulation equivalence, ready simulation
equivalence.
Esercizi per casa:
- Provare che il preordine di simulazione è un
preordine, una congruenza, implica la trace inclusion.
- Provare che il preordine di simulazione ready è un preordine,
una congruenza, implica la trace inclusion,e la complete trace
inclusion.
- Provare le inclusioni strette tra le varie equivalenze discusse
(simulation equivalence, ready equivalence, trace equivalence,
complete trace equivalence, bisimulation equivalence)
- Provare che la weak bisimilarity coincide con la strong
bisimilarity definita sul LTS weak
- Esercizi
-
Introduzione alla weak bisimilarity.
Fair abstraction from divergence e non osservabilità della
divergenza. Esercizio: buffer fifo con capacità
2. Esercizio 3.26. Proprieta` di congruenza della
bisimilarità debole.
Esercizi per casa: 3.27, 3.28, 3.29.
- Conguenza osservazionale.
Esercizi per casa:
- Formulazione dei 5 filosofi di Dijkstra che evita il deadlock
- dimostrare che la chiusura contestuale della bisimilarità
debole è la più grande congruenza che raffina
la bisimilarità debole
- dimostrare che la suddetta relazione è la congruenza
osservazionale (**)
-
Bisimilarità come massimo punto fisso.
Esercizi per casa:
- Verificare che se F è il funzionale della bisimulazione, allora le
relazioni F(n)(Proc x Proc) sono tutte
equivalenze
- Dimostrare che se D è un reticolo completo numerabile e
F : D -> D una funzione monotona allora il minimo punto fisso si
ottiene come supnF(n)(0), dove
0 è il minimo del reticolo.
-
Logica di Hennessy-Milner. Teorema di Hennessy-Milner.
Esercizi
- Logica di Hennessy-Milner con ricorsione
- Semantica formale della logica di Hennessy-Milner con ricorsione
ed esercizi
- Mutua esclusione in CCS
- Dal CCS al pi-calcolo
- Sintassi e semantica a riduzioni. Esempi.
- LTS per il pi-calcolo
- Bisimuazione forte e bisimulazione up to congruenza
strutturale
- Sistema di tipi semplici. Subtyping per distinguere capabilities
di lettura e scrittura sui canali. Uso dei tipi per ragionare sui
processi
- L'uso dei tipi nelle reti aperte: provare una proprieta' di
secrecy in presenza di componenti untrusted.
Modalità d'Esame e Appelli
L'esame consiste nello svolgimento di alcuni esercizi assegnati
durante l'anno e in un'attività di approfondimento finale,
che lo studente poi dovrà presentare in forma seminariale.
Più precisamente, la prova finale consiste nello svolgimento
di due esercizi e, a scelta, nella realizzazione di un mini-progetto
o nell'approfondimento di un argomento tra quelli elencati nel
seguito (temi alternativi, concordati con il docente sono comunque
possibili). Il tutto andrà presentato in forma seminariale,
in un tempo pari ad un'ora circa.
I temi d'esame si possono trovare qui.
Riferimenti bibliografici
Si utilizzerà il seguente libro
-
L. Aceto, A. Ingolfsdottir, K.G. Larsen, J. Srba
"Reactive systems"
Cambridge University Press, 2007
Per le lezioni sul pi-calcolo sono disponibili i seguenti appunti.
Un testo molto utile per consultazione è
- R. Milner
Communication and Concurrency
Prentice Hall, 1989.
Alcuni riferimenti per la parte sul pi-calcolo:
Link Utili
- Edimburgh
Concurrency Workbench
Uno strumento interattivo per la definizione, simulazione, prova
di proprietà di processi scritti in CCS (ed in varie estensioni
di questo).
- Sono disponibili i binari per Linux
- Può essere usato in emacs (consigliato),
seguendo le istruzioni specificate
qui.
- uDrawGraph (sostituto di daVinci)
Programma che permette la visualizzazione di transition graph in modo grafico nel Concurrency Workbench.
- scaricare la versione precompilata per Linux
- inserire la directory corrispondente in qualsiasi posizione
- settare la variabile di ambiente UDG_HOME al path della directory suddetta
- Bisimulation game and CCS
simulator
Permette di visualizzare e simulare il comportamento di un
processo dato il suo transition graph nel formato prodotto da
Concurrency Workbench e di giocare con le equivalenze
comportamentali.
- richiede di avere Java > 5 e il pacchetto graphViz
- usare la distribuzione fornita e aggiornare il file
properties.txt (indicando il path al binario dot di
graphViz)
- Concurrency Workbench of the new century
Offre funzionalità simili all'Edimburgh Concurrency
Workbench. Supporta vari linguaggi tra cui CCS, CCS con
priorità, timed CCS, CSP, Basic Lotos.
- Mobility Workbench
Simile ai Concurrency Workbench, ma supporta calcoli per la
mobilità come il pi-calcolo.