next up previous
Next: MC308 Semantics of Programming Up: Year 3 Previous: MC306 Programming Concurrent Computer

MC307 Communication and Concurrency


MC307 Communication and Concurrency

Credits: 20 Convenor: Dr. I. Ulidowski Semester: 2


Prerequisites: essential: MC111 desirable: MC103, MC306
Assessment: Continual assessment: 30% Three hour exam in June: 70%

Lectures: 30 Classes: none
Tutorials: 9 Private Study: 95
Labs: 16 Seminars: none
Project: none Other: none
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 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

Transferable Skills

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 for the continual assessment consists of five worksheets containing pencil and paper problems.

The written June examination contains six questions, and candidates can obtain full marks from four good questions.


next up previous
Next: MC308 Semantics of Programming Up: Year 3 Previous: MC306 Programming Concurrent Computer
S. J. Ambler
11/20/1999