Department of Mathematics & Computer Science

MC307 Communication and Concurrency

Explanation of Pre-requisites

Course Description

• each part acts concurrently with, and independently of, the other parts, and
• parts can also communicate (or interact) with each other to synchronize their behaviour or to exchange information.

This module introduces two formalisms for specifying, designing and analysing concurrent systems. It also provides the background for further study and research in concurrency, and in theories of distributed systems and real-times systems.

Aims

Objectives

• To understand the notions of concurrency, communication, mobility and concurrent systems.
• To have a good knowledge of CCS and the -calculus and their semantics.
• To be able to develop informal and formal specifications of simple concurrent systems, and to be able to derive designs from specifications.
• To be able to reason about the behaviour of simple concurrent systems, both by hand and with the aid of the Concurrency Workbench.

Transferable Skills

• The general understanding of concurrent systems and their development.
• The basic knowledge of concurrency theory.
• The ability to use CCS and the -calculus to specify and design simple concurrent systems.
• The experience in formal verification of systems via the use of the Concurrency Workbench.

Syllabus

Introduction. An introduction to concurrent and distributed systems, the notions of concurrency, communication and mobility, and a motivation for a formal theory of communication and concurrency.

Modelling concurrency and communication. An introduction, by means of examples, of the basic ideas and principles involved in modelling concurrency and communication. Transition rules and transition diagrams.

Process Algebras. Syntax and operational semantics of CCS and syntax and reduction rules of the -calculus.

Equational laws and algebraic reasoning. Equational laws for CCS and their justification. Techniques for equational reasoning.

Bisimulations Strong and weak bisimulations, strong and weak congruences (observational congruence). Techniques for establishing bisimulation equivalences, differences and relationships between various bisimulation relations. Compositional reasoning.

Case studies. Specifications and designs of simple concurrent systems in CCS and the -calculus.

Reading list

Essential:

R. Milner, Communicating and Mobile Systems: the -calculus, Cambridge University Press, 1999.

Recommended:

C.A.R. Hoare, Communicating Sequential Processes, Prentice-Hall 1985.

J.C. Baeten and W.P. Weijland, Process Algebra, Cambridge University Press 1990.

A.W. Roscoe, The Theory and Practice of Concurrency, Prentice-Hall 1997.

C. Fencott, Formal Methods for Concurrency, Thomson Computer Press 1996.

Background:

A. Burns and G. Davies, Concurrent Programming, Addison-Wesley 1993.

Details of Assessment

Author: S. J. Ambler, tel: +44 (0)116 252 3884
Last updated: 2001-09-20
MCS Web Maintainer
This document has been approved by the Head of Department.
© University of Leicester.