[The University of Leicester]

Department of Mathematics & Computer Science



Next: CO3008 Semantics of Programming Languages Up: Year 3 Previous: CO3001 Formal Software Specifications

CO3007 Communication and Concurrency

CO3007 Communication and Concurrency

Credits: 20 Convenor: Dr. I. Ulidowski Semester: 2
Prerequisites: essential: CO1011 desirable: CO1003
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

Subject Knowledge

Aims

This module provides 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 tool.

Learning Outcomes

Students should be able to: understand the notions of concurrency, communication, and concurrent systems; have a good knowledge of CCS and its operational and axiomatic semantics; be able to develop informal and formal specifications of simple concurrent systems, and be able to produce systems' designs from specifications; able to reason about the behaviour of simple concurrent systems, both by hand and with the aid of the Concurrency Workbench, using the techniques of equational reasoning and bisimulation.

Methods

Class and laboratory sessions together with course notes (available on the Web and in the printed form), Bisimulation Games workshop, recommended textbooks, the Concurrency Workbench manual, class and laboratory worksheets, printed solutions, and web support.

Assessment

Marked coursework, traditional written examination.

Subject Skills

Aims

To teach students problem solving and scientific writing skills.

Learning Outcomes

Students will be able to: solve abstract and concrete problems (both routine seen, and simple unseen); write short summaries of technical material

Methods

Class and laboratory sessions, course notes and text books, software manuals, class and laboratory worksheets, printed solutions.

Assessment

Marked coursework, traditional written examination.

Explanation of Pre-requisites

Basic knowledge of discrete mathematics and logic is essential.

Course Description

A concurrent system is a system consisting 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 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.

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, to the basic ideas and principles involved in the modelling of concurrency and communication. Transition rules, inference trees and transition graphs.

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. Verification of correctness using the Concurrency Workbench tool.

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.

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

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

S. Schneider, Concurrent and Real-time Systems, Wiley 2000.

W. Fokkink, Introduction of Process Algebra, Springer 2000.

C. Stirling, Modal and Temporal Properties of Processes, Springer 2001.

Resources

Course notes, text books in library, study guide, worksheets, handouts, past examination papers, module web pages, lecture rooms with OHPs, laboratories with PCs and demonstrators, the Concurrency Workbench software tool, surgeries.

Module Evaluation

Course questionnaires, course review.

Next: CO3008 Semantics of Programming Languages Up: Year 3 Previous: CO3001 Formal Software Specifications

[University Home] [MCS Home] [University Index A-Z] [University Search] [University Help]

Author: N. Rahman, tel: +44 (0)116 252 3902
Last updated: 2003-09-23
MCS Web Maintainer
This document has been approved by the Head of Department.
© University of Leicester.