Home » Archivo » Archvio 2013 » LINGUAGGI E MODELLI PER IL GLOBAL COMPUTING - 2013/2014

Laurea Magistrale

Salta il menu di secondo livello

LINGUAGGI E MODELLI PER IL GLOBAL COMPUTING - 6 CFU - A.A. 2013/2014

Insegnante

Prof. Paolo Baldan

Periodo

I Anno - 2 Trimestre | 13/01/2014 - 15/03/2014

Ore: 48 (48 lezione)

Torna su ▲

Prerequisiti

Il corso richiede familiarità con alcuni concetti matematici di base, quali relazioni, funzioni, insiemi, cardinalità, ordini parziali, principi di induzione, sistemi di deduzione basati su regole di inferenza. Sono utili alcune conoscenze di semantica dei linguaggi di programmazione.
Il corso non ha propedeuticità.

Conoscenze e abilità da acquisire

L'enorme diffusione dei sistemi concorrenti, distribuiti e mobili rende inadeguati i paradigmi di specifica e programmazione classici ed apre sfide complesse e affascinanti. Appare necessario un ripensamento, che parta dalle stesse fondamenta e che adotti un approccio rigoroso, formale, disciplinato. Il corso si propone di avvicinare lo studente a tematiche di interesse in questo ambito, utilizzando come strumenti sistemi di tipi, calcoli di processo e in generale linguaggi di modellazione. Parte da argomenti fondazionali oramai classici (come il Calculus of Communicating Systems ed il pi-calculus) e giunge ad illustrare alcuni argomenti di punta della ricerca nell'area. Vengono discussi alcuni linguaggi che traducono in pratica gli sviluppi teorici descritti, quali linguaggi evoluti per la concorrenza (Google Go, Erlang), linguaggi di orchestrazione (ORC) e linguaggi per programmazione service oriented (Jolie).

Modalità di esame

Esercizi in classe, soluzione e discussione orale di esercizi avanzati, presentazione di un tema scelto dallo studente. Tra le opzioni ci sarà anche la realizzazione di un piccolo progetto che usi uno strumento di verifica.

Criteri di valutazione

Lo studente è valutato rispetto alla sua capacità di risolvere semplici esercizi, verificando così l'acquisizione di nozioni e tecniche discusse durante il corso. Alcuni esercizi avanzati sono finalizzati a verificare la capacità di mettere a frutto quanto appreso per la soluzione di problemi nuovi. La presentazione verifica l'abilità dello studente di approfondire, autonomamente, tematiche di ricerca nell'area di interesse per il corso, e di esporre in modo efficace quanto appreso.

contenuti

La struttura e le tematiche del corso saranno le seguenti:

- Introduzione alla concorrenza e mobilità: dagli automi ai sistemi reattivi e concorrenti.

- Calculus of Communicating Systems (CCS), un linguaggio minimale per la descrizione di sistemi concorrenti. Equivalenza di processi: Sistemi di transizione e bisimulazione.

- Logica di Hennessy-Milner e strumenti per la verifica. Mutua esclusione, deadlock, fairness. Proprietà di safety e liveness.

- Verifica di proprietà con strumenti automatici. Il Concurrency Workbench ed il Mobility Workbench.

- Sistemi con topologia dinamica e mobilità: pi-calcolo. Specifica di proprietà spaziali e cenni di applicazioni alla sicurezza dei protocolli.

- Dai linguaggi di specifica ai linguaggi di programmazione: linguaggi avanzati per la concorrenza (Google Go, Erlang), linguaggi di orchestrazione (ORC) e linguaggi per programmazione orientata ai servizi (Jolie).

Attività di apprendimento previste e metodologie di insegnamento

Lezioni in classe e uso di strumenti di verifica automatica.

Eventuali indicazioni sui materiali di studio

Il libro di testo è complementato con articoli di ricerca e altre risorse disponibili online.
Pagina web: http://www.math.unipd.it/~baldan/Global

Testi di riferimento

Torna su ▲