CODE 
CPS5122 

TITLE 
Principles of Concurrency 

LEVEL 
05  Postgraduate Modular Diploma or Degree Course 

ECTS CREDITS 
5 

DEPARTMENT 
Computer Science 

DESCRIPTION 
In order to be able to construct correct, efficient and dependable software for distributed systems, serviceoriented systems and multicore machines, engineers require a deep understanding of the fundamental concepts of concurrency. This course thus takes a formal approach to the modelling, specification and verification of concurrent systems. It explains how concurrent systems can be described in terms of statetransition models such as labelled transition systems and uses process calculi to model the behaviour of such concurrent systems. Correctness specification and verification is tackled both from the point of view of language equivalence, but also through the use of modal logics.
Studyunit Aims:
1. To familiarise the student with the main issues and characteristics of concurrent systems, such as nondeterminism and reactive, nonterminating computation; 2. To show how these aspects affect correctness specification and verification; 3. To teach powerful mathematical tools such as induction and coinduction, and to show how these can be applied to formally reason about these systems; 4. To expose the student to algorthmic solutions to the verification of these systems.
Learning Outcomes:
1. Knowledge & Understanding: By the end of the studyunit the student will be able to:
 describe a concurrent reactive system's behaviour formally using a Labelled Transition System;  apply conductive reasoning so as to construct a bisimulation exhibiting the equivalence of two systems. If, conversely, the two systems are not equivalent, the student could also justify their inequality by exhibiting a game strategy that proves the inexistent of a satisfying bisimulation relation;  formulate properties using modal logics and prove the satisfaction or otherwise of the property of a formally specified system.
2. Skills: By the end of the studyunit the student will be able to:
 model (concurrent) systems and computation at different levels of abstraction;  apply compositional design and analysis to programs.
Main Text/s and any supplementary readings:
Textbook:  Reactive Systems: Modelling, Specification and Verification. Luca Aceto, Anna Ingolfsdottir, Kim Guldstand Larsen, Jiri Srba Cambridge University Press 2007 ISBN: 9780521875462
References:
 Communicating and mobile systems: the Picalculus Robin Milner Cambridge University Press 1999 ISBN 0521658691  Introduction to Bisimulation and Coinduction Davide Sangiorgi Cambridge University Press 2012 ISBN 9781107003637  Modal and Temporal Properties of Processes Colin Sterling Springer 2001 ISBN 0387987177


RULES/CONDITIONS 
Before TAKING THIS STUDYUNIT YOU MUST TAKE CPS3238 OR TAKE CSA3217 

STUDYUNIT TYPE 
Lecture and Tutorial 

METHOD OF ASSESSMENT 
Assessment Component/s 
Resit Availability 
Weighting 
Examination
(2 Hours and 30 Minutes)

Yes 
100% 


LECTURER/S 
Adrian Francalanza


The University makes every effort to ensure that the published Courses Plans, Programmes of Study and StudyUnit information are complete and uptodate at the time of publication. The University reserves the right to make changes in case errors are detected after publication.
The availability of optional units may be subject to timetabling constraints.
Units not attracting a sufficient number of registrations may be withdrawn without notice.
It should be noted that all the information in the studyunit description above applies to the academic year 2017/8, if studyunit is available during this academic year, and may be subject to change in subsequent years.

19 October 2017
http://www.um.edu.mt/ict/studyunit