| CODE | CPS5122 | ||||||
| TITLE | Principles of Concurrency | ||||||
| UM LEVEL | 05 - Postgraduate Modular Diploma or Degree Course | ||||||
| MQF LEVEL | 7 | ||||||
| ECTS CREDITS | 5 | ||||||
| DEPARTMENT | Computer Science | ||||||
| DESCRIPTION | In order to be able to construct correct, efficient and dependable software for distributed systems, service-oriented systems and multi-core 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 state-transition 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. Study-unit Aims: 1. To familiarise the student with the main issues and characteristics of concurrent systems, such as non-determinism and reactive, non-terminating 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 study-unit 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 study-unit 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: 978-0-521-87546-2 References: - Communicating and mobile systems: the Pi-calculus Robin Milner Cambridge University Press 1999 ISBN 0-521-65869-1 - Introduction to Bisimulation and Coinduction Davide Sangiorgi Cambridge University Press 2012 ISBN 978-1-107-00363-7 - Modal and Temporal Properties of Processes Colin Sterling Springer 2001 ISBN 0-387-98717-7 |
||||||
| RULES/CONDITIONS | Before TAKING THIS UNIT YOU MUST TAKE CPS3238 OR TAKE CSA3217 | ||||||
| STUDY-UNIT TYPE | Lecture and Tutorial | ||||||
| METHOD OF ASSESSMENT |
|
||||||
| LECTURER/S | Adrian Francalanza |
||||||
|
The University makes every effort to ensure that the published Courses Plans, Programmes of Study and Study-Unit information are complete and up-to-date 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 description above applies to study-units available during the academic year 2023/4. It may be subject to change in subsequent years. |
|||||||