COSTRUTTI LINGUISTICI E TECNICHE DI VERIFICA PER SISTEMI CONCORRENTI
Specialistica di Informatica, AA. 2006/2007

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.

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 decidibilita' di equivalenze osservazionali. Specifica e verifica di proprieta': Hennessy-Milner logic. Sicurezza: information flow security e non-interferenza. Segretezza autenticazione e integrita' in crypto-protocols.
Modulo 2:
Il problema della mobilita' in sistemi concorrenti, distribuiti, ad oggetti e in = reti wireless. Un approccio semantico alla mobilita': 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

Materiale didattico

Per la prima parte del corso, lucidi in pdf.

Modalita' esame

Prova orale, di solito in forma seminariale su argomento concordato con uno dei due docenti.

Orario di Ricevimento

Consultare le pagine personali dei docenti