COM3190 Theory of Distributed Systems
|| The aim of this module is to set out a
strong theoretical basis for the analysis and design of
concurrent, distributed and mobile systems. We will use the
process calculi to model and reason about complex systems,
studying both its formal semantics and its many uses, via a
number of examples. Students should be aware that there are limited places available on this course.
- Formal examination (LOs 1-5)
||Dr Harsh Beohar
The aims of this module are:
- to develop an understanding of the subtleties of
concurrent and mobile systems' behaviours;
- to develop an understanding of the formal semantics of process algebras;
- to develop the ability to construct models of simple
systems in these calculi, and where appropriate to use
software tools to investigate their properties;
- to develop the ability to reason about system behaviour using process algebras and related logics.
|| By the end of this course the students should:
- appreciate the fundamental techniques and principles
needed to formally specify languages for concurrency;
- understand the mathematical theory underlying process calculus and be able to apply it to concrete
- be able to construct concurrent specifications from
requirements, to transform and analyse them using
appropriate tools and techniques, and to apply these
skills to problems drawn from a number of different
- appreciate the scope and limits of algebraic
techniques in the analysis of concurrency;
- have developed their ability to critically evaluate
their work and to discuss it coherently with others; and have expanded their capacity to model, reason
about and evaluate complex systems.
Sequential vs concurrent systems; real vs interleaving
concurrency; mobile systems.
2. BASIC PROCESS ALGEBRA
- Using simple equations to represent complex systems;
synchronisation and non-determinism; structured
operational semantics; flow diagrams and transition
diagrams; simulation and bisimulation; the importance of
hidden internal actions.
- Detailed examples: modelling a conversation; modelling
an n-place buffer.
- Modal logics, model checkers and workbenches: using
software to reason about concurrent systems.
3. INTERLUDE: Other approaches
- CCS, CSP, Petri nets, Mazurkiewicz traces; P systems and
other bio-inspired models.
4. THEORY OF COMMUNICATING PROCESSES
- Adding mobility to; transition rules; replication
vs recursion; scope extrusion; process equivalence.
- Optional: The computational power of pi-calculus: representing
data types and functions as pi-calculus processes.
- Optional: Variations on a theme: stochastic pi, security and
ambients, modelling the flow of encrypted data.
5. DETAILED CASE STUDY
A case study illustrating the techniques used in modelling real-world situations.
||Strong grasp of mathematical logic.
|| In addition to lectures, the course will include exercise
sheets and tutorial sessions; these will cover the course material. In a dedicated lecture, the theory will be applied using a modelling language to analyse concurrent process behaviours.
|| Students will receive feedback in lectures and during the
weekly lab sessions. Weekly exercise sheets will also be
provided to help students assess their own progress.
A list of relevant sources will be provided on the Blackboard webpages.
Lecture notes will be available through Blackboard.
important older titles include:
- J.C.M. Baeten, M.A. Reniers and T. Basten(2009). Process Algebra: Equational Theories of Communicating Processes. CUP
- Robin Milner (1999) Communicating and Mobile Systems:
The Pi Calculus. CUP.
- Davide Sangiorgi (2003) The Pi-Calculus: A Theory of
Mobile Processes. CUP.
- Robin Milner, Joachim Parrow and David Walker (1989,
revised 1990) A Calculus of Mobile Processes, Part I. Tech. Report ECS-LFCS-89-85, Laboratory for the
Foundations of Computer Science, Edinburgh University. Available online at: http://www.lfcs.informatics.ed.ac.uk/reports/89/ECS-LFCS-89-85/
- Robin Milner (1985) Communication and Concurrency.
- C.A.R. Hoare (1985) Communicating Sequential
Processes. Prentice Hall.
Available online at: http://www.usingcsp.com/cspbook.pdf
- Formal Aspects of Computing
- Theoretical Computer Science
- Lecture Notes in Computer Science