The University of Sheffield
Department of Computer Science

COM6116 Theory of Distributed Systems

Summary 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. You should be aware there are limited places on this course.
Session Spring 2023/24
Credits 15
Assessment
  • Formal examination (LOs 1-5)
Lecturer(s) Dr Harsh Beohar
Resources
Aims

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.
Learning Outcomes  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 examples;
  • be able to construct concurrent specifications from requirements, to refine them using algebraic techniques, and to apply these skills to problems drawn from a number of different fields;
  • analyse the scope and limits of algebraic techniques in 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.
Content

1. INTRODUCTION
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.
Essential skills Strong grasp of mathematical logic.
Teaching Method 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.
Feedback 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.