![[The University of Leicester]](http://www.le.ac.uk/corporateid/departmentresource/000066/unilogo.gif) | Department of Mathematics & Computer Science |
 |
Next: MC308 Semantics of Programming Languages
Up: Year 3
Previous: MC306 Programming Concurrent Computer Systems
MC307 Communication and Concurrency
| Credits: 20 |
Convenor: Dr. I. Ulidowski |
Semester: 2 |
| Prerequisites: |
essential: MC111 |
desirable: MC103, MC306 |
| Assessment: |
Coursework: 30% |
Three hour exam in May/June: 70% |
| Lectures: |
36 |
Problem Classes: |
none |
| Tutorials: |
none |
Private Study: |
96 |
| Labs: |
6 |
Seminars: |
none |
| Project: |
none |
Other: |
none |
| Surgeries: |
12 |
Total: |
150 |
Explanation of Pre-requisites
It is essential that students have studied discrete mathematics
and logic, and have had some experience in sequential and concurrent
programming.
Course Description
A concurrent system is a dynamic system which is composed
of several parts such that
- 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 and exchange information.
In recent years there has been much interest and demand for concurrent
systems such as, for example, communication networks, air traffic controllers
and industrial plant control systems. As such systems are often very complex
and essential in our everyday life, it is vital that they are highly reliable.
Therefore, there is an ever growing need for formalisms and software tools for
design and construction of reliable concurrent systems.
This module introduces a formalism for specifying, designing, implementing and
analysing concurrent systems.
It also provides the background for further study and research in concurrency,
and in theories of distributed systems, real-times systems and
fault-tolerant systems.
Aims
This module will provide students with an introduction to theories
and applications of concurrency. In particular, it will familiarise students
with the process algebra Calculus of Communicating Systems,
or CCS for short, and its operational and axiomatic semantics. The module will
teach, via individual and collective work, how to specify, design
and implement simple concurrent systems. Students will also learn how to
verify correctness of systems using the Concurrency Workbench.
Objectives
- To understand the basic nature of concurrent systems.
- To have a good knowledge of CCS and its semantics.
- To be able to develop informal and formal specifications of simple
concurrent systems, and from them derive implementations.
- To be able to reason about the behaviour of simple 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 a theory of concurrency.
- The ability to use CCS to specify and implement simple
concurrent systems.
- The experience in formal verification and in the use of
the Concurrency Workbench.
Syllabus
Introduction. An introduction to concurrent and distributed systems,
the notions of concurrency and communication, motivations 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 diagrams.
CCS. Formal definitions of syntax and semantics of CCS.
Equational laws and algebraic reasoning. Equational laws and their
justification; techniques for algebraic 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 implementations of
simple concurrent systems in CCS.
Reading list
Essential:
R. Milner,
Concurrency and Communication,
Prentice-Hall 1989.
Recommended:
C.A.R. Hoare,
Communicating Sequential Processes,
Prentice-Hall 1985.
J.C. Baeten and W.P. Wiejland,
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.
M. Ben-Ari,
Principles of Concurrent and Distributed Programming,
Prentice-Hall 1990.
Details of Assessment
The coursework consists of six worksheets
containing pencil and paper problems.
The written June examination contains six questions, and candidates can
obtain full marks for good answers to four questions.
Next: MC308 Semantics of Programming Languages
Up: Year 3
Previous: MC306 Programming Concurrent Computer Systems
Author: S. J. Ambler, tel: +44 (0)116 252 3884
Last updated: 10/4/2000
MCS Web Maintainer
This document has been approved by the Head of Department.
© University of Leicester.
![[University Home]](http://www.le.ac.uk/corporateid/navigation/unihome.gif){kind=small}
![[MCS Home]](http://www.le.ac.uk/corporateid/navigation/depthome.gif){kind=small}
![[University Index A-Z]](http://www.le.ac.uk/corporateid/navigation/index.gif){kind=small}
![[University Search]](http://www.le.ac.uk/corporateid/navigation/search.gif){kind=small}
![[University Help]](http://www.le.ac.uk/corporateid/navigation/help.gif){kind=small}