![[The University of Leicester]](http://www.le.ac.uk/corporateid/departmentresource/000066/unilogo.gif) | Department of Mathematics & Computer Science |
 |
Next: CO3008 Semantics of Programming Languages
Up: Level 3
Previous: CO3001 Formal Software Specifications
CO3007 Communication and Concurrency
| Credits: 20 |
Convenor: Dr. I. Ulidowski |
Semester: 1 |
| Prerequisites: |
essential: CO1011 |
desirable: CO1003 |
| Assessment: |
Coursework: 30% |
Three hour exam in January: 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.
Course Description
A concurrent system is a system consisting
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 or to 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 concurrent systems are often very complex
and essential in our everyday life, it is vital that they are highly reliable.
Therefore, there is a growing need for formalisms and software tools that can assist
us in the design and construction of reliable concurrent 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 algebras CCS (Calculus of Communicating Systems)
and its operational 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 concurrent systems using
the Concurrency Workbench software
package.
Objectives
- To understand the notions of concurrency, communication,
and 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 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 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.
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.
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. 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.
Details of Assessment
The coursework consists of several worksheets
containing pencil and paper problems.
The written examination contains six questions, and candidates can
obtain full marks for good answers to four questions.
Next: CO3008 Semantics of Programming Languages
Up: Level 3
Previous: CO3001 Formal Software Specifications
Author: S. J. Ambler, tel: +44 (0)116 252 3884
Last updated: 2002-07-11
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}