Corsi di Laurea Corsi di Laurea Magistrale Corsi di Laurea Magistrale
a Ciclo Unico
Scuola di Scienze
INFORMATICA
Insegnamento
LINGUAGGI E MODELLI PER IL GLOBAL COMPUTING
SCM0018214, A.A. 2015/16

Informazioni valide per gli studenti immatricolati nell'A.A. 2015/16

Principali informazioni sull'insegnamento
Corso di studio Corso di laurea magistrale in
INFORMATICA
SC1176, ordinamento 2014/15, A.A. 2015/16
N0
porta questa
pagina con te
Crediti formativi 6.0
Tipo di valutazione Voto
Denominazione inglese LANGUAGES AND MODELS FOR GLOBAL COMPUTING
Sito della struttura didattica http://informatica.scienze.unipd.it/2015/laurea_magistrale
Dipartimento di riferimento Dipartimento di Matematica
Obbligo di frequenza No
Lingua di erogazione ITALIANO
Sede PADOVA
Corso singolo È possibile iscriversi all'insegnamento come corso singolo
Corso a libera scelta È possibile utilizzare l'insegnamento come corso a libera scelta

Docenti
Responsabile PAOLO BALDAN INF/01

Dettaglio crediti formativi
Tipologia Ambito Disciplinare Settore Scientifico-Disciplinare Crediti
CARATTERIZZANTE Discipline Informatiche INF/01 6.0

Organizzazione dell'insegnamento
Periodo di erogazione Secondo semestre
Anno di corso I Anno
Modalità di erogazione frontale

Tipo ore Crediti Ore di
didattica
assistita
Ore Studio
Individuale
LEZIONE 6.0 48 102.0

Calendario
Inizio attività didattiche 01/03/2016
Fine attività didattiche 15/06/2016
Visualizza il calendario delle lezioni Lezioni 2019/20 Ord.2014

Commissioni d'esame
Nessuna commissione d'esame definita

Syllabus
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 abilita' 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).
Modalita' 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).
Attivita' 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:
  • R. Milner, Communication and Concurrency. --: Prentice Hall, 1989. Testo di consultazione, disponibile in biblioteca Cerca nel catalogo
  • L. Aceto, A. Ingolfsdottir, K.G. Larsen, J. Srba, Reactive systems. --: Cambridge University Press, 2007. Testo adottato, si utilizzeranno i capitoli 1-7. Cerca nel catalogo