
Course unit
LANGUAGES AND MODELS FOR GLOBAL COMPUTING
SCM0018214, A.A. 2015/16
Information concerning the students who enrolled in A.Y. 2015/16
ECTS: details
Type 
ScientificDisciplinary Sector 
Credits allocated 
Core courses 
INF/01 
Computer Science 
6.0 
Course unit organization
Period 
Second semester 
Year 
1st Year 
Teaching method 
frontal 
Type of hours 
Credits 
Teaching hours 
Hours of Individual study 
Shifts 
Lecture 
6.0 
48 
102.0 
No turn 
Examination board
Examination board not defined
Prerequisites:

The course requires some familiarity with basic mathematical concepts such as relations, functions, sets, cardinality, partial orders, principles of induction, deduction systems based on inference rules. Some basic knowledge of programming language semantics are useful.
There are no propaedeutical courses. 
Target skills and knowledge:

The widespread diffusion of concurrent, distributed and mobile systems makes the classical programming and specification paradigms inadequate and opens complex and fascinating challenges. A rethinking appears necessary, starting from the foundations and adopting a rigorous, formal and disciplined approach. The aim of the course is to introduce the student to themes of interest in the area, using as tools type systems, process calculi and modelling languages in general. Starting from topics which are by now classical (like the Calculus of Communicating Systems and picalculus), we will reach some advanced issues of the research in the area. Some languages that implement the theoretical developments discussed are presented, including advanced languages for concurrency (Google Go, Erlang), orchestration languages (ORC) and languages for service oriented programming (Jolie). 
Examination methods:

Class exercises, solution and oral discussion of some advanced exercises, presentation on a theme choosen by the student. Among the options, there is the possibility of realizing a small project using a tool for formal verification. 
Assessment criteria:

The student is evaluated on his ability of solving simple exercises, witnessing the acquisition of the notions and techniques exposed in the course. Some advanced exercises test the ability of using the acquired expertise in the solution of new problems. The presentation verifies the capability of the student of deepening, autonomously, research themes in the area of interest and of properly exposing what she learnt. 
Course unit contents:

The structure and themes of the course will be as follows:
 Introduction to concurrency and mobility: from automata to reactive and concurrent systems.
 Calculus of Communicating Systems (CCS), a basic language for the description of concurrent systems. Process equivalence: transition systems and bisimulation.
 HennessyMilner logic and tools for verification. Mutual exclusion, deadlock freeness, fairness. Safety and liveness properties.
 Verification of properties with automated tools. The Concurrency Workbench and the Mobility Workbench.
 Systems with dynamic topology and mobility: picalculus. Specification of spatial properties and applications to protocol security.
 From specification languages to programming languages: advanced languages for concurrency (Google Go, Erlang), orchestration languages (ORC) and languages for serviceoriented programming (Jolie). 
Planned learning activities and teaching methods:

Lectures and use of tools for automatic verification. 
Additional notes about suggested reading:

The textbook is complemented with research papers and online resources.
Web page: http://www.math.unipd.it/~baldan/Global 
Textbooks (and optional supplementary readings) 

R. Milner, Communication and Concurrency. : Prentice Hall, 1989. Testo di consultazione, disponibile in biblioteca

L. Aceto, A. Ingolfsdottir, K.G. Larsen, J. Srba, Reactive systems. : Cambridge University Press, 2007. Testo adottato, si utilizzeranno i capitoli 17.


