Aim

The widespread diffusion of concurrent, distributed and mobile systems makes the classical programming and specification paradigms inadequate and opens up 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 pi-calculus that center the study around some basic concepts like processes, composition and communication mechanisms), 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 and distribution like Google Go, Erlang, Elixir, Clojure, Jolie, Rust, along with the corresponding programming techniques.

Program

The structure and themes of the course will be as follows:

1. The "Calculus of Communicating Systems" (CCS), a core language for the description of concurrent systems. Process equivalence: transition systems and bisimulation.
2. Hennessy-Milner logic and tools for verification. Mutual exclusion, deadlock, fairness. Safety and liveness properties. Systems with dynamic topology and mobility: pi-calculus. Verification tools (Concurrency Workbench, Caal, PseuCo).
3. From specification languaes to programming langauges: Google Go, Erlang, Elixir, Clojure, Rust, Jolie, ORC.

Schedule

This is a course unit of the Master's Degree In Computer Science, University of Padua, and it is held in the 2nd semester for the A.Y. 2023/2024, with the folling schedule. Adjustments if there are common requests by the participants.

Day	Time	Room
Monday	14.30 - 16.00	1BC/50
Tuesday	12.30 - 14.00	1BC/50

Exam

The exam consists of two parts: exercises and a deepening/project (see below), to be prepared off-line and then presented in an oral discussion/seminar.

1. EXERCISES
   You should do two exercises in the section Exercises in the following page
2. DEEPENING/PROJECT
   You can choose among various possibilities including (1) a mini-project consisting in the specification / implementation / verification of a system and its formal properties (2) the study of advanced verification tools (3) study of research papers about formal models, verification techniques, programming languages related to the themes of the course. Again, some ideas can be found at the following the page.

in both cases, the list of suggestions is not exhaustive. The student can propose different project ideas that better fit her/his personal interests (including different exercises, for example chosen from the book). In any case, the student's choices need to be discussed with the instructor, approved and defined in the details (the descriptions above are often sketchy). During the exam, that will last indicatively on hour, the student will solve the execises (typically, using the blackboard) and present the deepening/project part (for this, part, a slide-based presentation is typically useful).

Material

The course has a Moodle where additional material can be found. For the foundational part we will use the following book

• L. Aceto, A. Ingolfsdottir, K.G. Larsen, J. Srba
  "Reactive systems"
  Cambridge University Press, 2007 (Chap. 1-7, except 6.4)

The material concerning the part on programming languages will be distributed via the moodle.

Useful links

• Caal
  A web version of the concurrency workbench. This works on the most common browsers.
• PseuCo
  An interactive tool for defining and simulating processes written in a concurrent language (a sort of simplified Go langauge), which has an immediate translation into CCS.
• Edimburgh Concurrency Workbench
  An interactive tool for the definition, simulation and verification of properties of CCS processes (and of various CCS extensions).
  • Linux binaries are available (unfortunately 32-bit)
  • Can be compiled using the current version of SML New Jersey
  • It can be used in emacs (suggested), following the instructions here.
  • syntax highlighting for cwb (based on the package generic-x) cwb-highlight.el

• Bisimulation game and CCS simulator
  It allows one to visualise and simulate the behaviour of a process, given its transition graph as produced by the Concurrency Workbench and of playing with beavioural equivalences.
• Concurrency Workbench of the new century
  It offers functionalities similar to the Edimburgh Concurrency Workbench. It supports various languages like CCS, CCS with priorities, timed CCS, CSP, Basic Lotos.
• TAPAS a tool with a graphical interaface for studying CCSP processes (a language arising from the join of CCS and CSP). It offers also various plugins for stochastic calculi and calculi with code mobility.
• SLMC (spatial logic model checker). A tool for the verification of spatial properties of concurrent processes.
• Mobility Workbench
  Similar to the Concurrency Workbench, but it suports calculi for mobility, like the pi-calculus.

Some advanced tools

• CADP (Construction and Analysis of Distributed Processes)
• MCRL2 (micro Common Representation Language 2)
• PAT (Process Analysis Toolkit An Enhanced Simulator, Model Checker and Refinement Checker for Concurrent and Real-time Systems)