COSTRUTTI LINGUISTICI E TECNICHE DI VERIFICA PER
SISTEMI CONCORRENTI
Specialistica di Informatica,
AA. 2005/2006
Docenti
Roberto Gorrieri,
Davide Sangiorgi.
Scopo del corso
Fornire le conoscenze di base su problemi di specifica e verifica per
sistemi concorrenti, distribuiti e mobili.
Programma/Contenuti:
Il corso si compone di 2 moduli, il primo tenuto da Roberto Gorrieri,
il secondo da Davide Sangiorgi.
Sotto e' una breve descrizione dei 2 moduli.
Per altre informazioni sui moduli vedere:
- modulo 1 (link ancora da attivare)
-
modulo 2
Breve descrizione del corso:
Modulo 1:
Linguaggi di base per la descrizione di processi concorrenti. Il
linguaggio CCS: sintassi e semantica operazionale strutturata. Sistemi
di transizione etichettati. Equivalenze
osservazionali. Bisimulazione. Assiomatizzazione e decidibilitą di
equivalenze osservazionali.
Specifica e verifica di proprietą: Hennessy-Milner logic.
Sicurezza: information flow security e non-interferenza. Segretezza,
autenticazione e integritą in crypto-protocols.
Modulo 2:
Il problema della mobilitą in sistemi concorrenti, distribuiti,
adoggetti e in reti wireless. Un approccio semantico alla mobilitą: il
linguaggio pi-calcolo. Aspetti distintivi del linguaggio. Semantica
operazionale e osservazionale. Utilizzo del pi-calcolo per modellare
varie forme di sistemi concorrenti, ad esempio processi che migrano da
un sito ad un altro. Relazione tra pi-calcolo e lambda-calcolo
(programmazione funzionale sequenziale). Cenni all'utilizzo del
pi-calcolo per la descrizione di sistemi complessi in biologia.
Testi/Bibliografia
-
R. Milner, Communication and Concurrency, Prentice-Hall, 1989.
-
R. Milner, Communicating and Mobile Systems: the pi-calculus, Cambridge
University Press, 1999.
-
AA.VV.
-
Process Algebra Handbook, North-Holland, 2001.
-
D.Sangiorgi, D.Walker, The Pi-Calculus -- A Theory of Mobile Processes,
Cambridge University Press, 2001.
Modalita' esame
Prova orale
Orario di Ricevimento
Consultare le pagine personali dei docenti