Presentazione

Organizzazione della Didattica

DM270
INFORMATICA ORD. 2014


6

Corsi comuni

 

Frontali Esercizi Laboratorio Studio Individuale
ORE: 48 0 0 102

Periodo

AnnoPeriodo
I anno2 semestre

Frequenza

Facoltativa

Erogazione

Convenzionale

Lingua

Italiano

Calendario Attività Didattiche

InizioFine
26/02/201801/06/2018

Tipologia

TipologiaAmbitoSSDCFU
caratterizzanteDiscipline informaticheINF/016


Responsabile Insegnamento

ResponsabileSSDStruttura
DA ASSEGNAREN.D.

Altri Docenti

DocenteCoperturaSSDStruttura
Prof. BALDAN PAOLOIstituzionaleINF/01Dipartimento di Matematica

Attività di Supporto alla Didattica

Non previste.

Bollettino

Il corso non ha propedeuticità.

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, Clojure), linguaggi di orchestrazione (ORC) e linguaggi per programmazione service oriented (Jolie).

Lezioni in classe e uso di strumenti di verifica automatica.

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 con strumenti automatici. Il Concurrency Workbench e CAAL. - Dai linguaggi di specifica ai linguaggi di programmazione: linguaggi avanzati per la concorrenza (Google Go e channel-based concurrency, Erlang e modello ad attori, Clojure e functional concurrency) - Linguaggi di orchestrazione (ORC) e linguaggi per programmazione orientata ai servizi (Jolie).

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.

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.

CONTENUTO NON PRESENTE

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