Concurrent System Analysis & Verification - COM00020H

« Back to module search

  • Department: Computer Science
  • Module co-ordinator: Prof. Ana Cavalcanti
  • Credit value: 10 credits
  • Credit level: H
  • Academic year of delivery: 2017-18

Module summary

In the Spring term, this module covers the use of a process algebra for modelling, validation, design, and verification of concurrent reactive systems; in particular, it focusses on CSP (Communicating Sequential Processes) and Circus, which combines Z and CSP to model data-rich reactive programs, and is the main object of this module. Tools are used to illustrate the techniques, and facilitate learning of concepts. For validation by animation, we use ProBE (an animator for CSP), and for formal validation and verification, we use FDR (the CSP model checker). The main objective of the module is to study refinement: the concept and the associated techniques to validate and verify programs. We discuss the refinement-based models of CSP, model checking by refinement, and study Circus, a data-rich process algebra, to discuss data refinement.

Module will run

Occurrence Teaching cycle
A Spring Term 2017-18

Module aims

Software should do what you expect as reliably as any other technology. Usually it does not, however. Software is often unreliable and fails to meet the requirements. Typical software defect rates are unacceptable for any other kind of product. This module covers the modelling, validation, design, and verification techniques that contemporary engineers can employ to save money and time, and reduce risks. Specific aims of this module are to:

  • Describe a coherent set of techniques and tools that support the practical development of programs correct by construction.
  • Cover concurrent, and reactive programs.
  • Discuss the principles that justify the main techniques.
  • Illustrate the techniques with realistic case studies.

Module learning outcomes

On completion of this module, students will:

  • Read and write descriptions of specifications and designs of concurrent and reactive systems;
  • Use animation to validate specifications and designs;
  • Understand the models that support program development;
  • Understand refinement as a relation that captures the concept of correctness in the various models;
  • Analyse specifications and verify designs using refinement and model checking;
  • Develop programs that are guaranteed to meet their contracts.

Module content

Based on two process algebras for refinement: CSP and Circus, covering modelling, their semantics, and use of tools for model checking.

Assessment

Task Length % of module mark
University - closed examination
Concurrent System Analysis & Verification
N/A 100

Special assessment rules

None

Additional assessment information

Formative assessments are part of the practical sessions. They are handed in and the marked work is discussed on an individual basis in the following session

Reassessment

Task Length % of module mark
University - closed examination
Concurrent System Analysis & Verification
N/A 100

Module feedback

A number of formative assessments (typically four) in the Spring Term.

Indicative reading

A. W. Roscoe, Understanding Concurrent Systems, Springer, 2011

S. Schneider. Concurrent and Real-time Systems: The CSP Approach. Wiley, 2005.



The information on this page is indicative of the module that is currently on offer. The University is constantly exploring ways to enhance and improve its degree programmes and therefore reserves the right to make variations to the content and method of delivery of modules, and to discontinue modules, if such action is reasonably considered to be necessary by the University. Where appropriate, the University will notify and consult with affected students in advance about any changes that are required in line with the University's policy on the Approval of Modifications to Existing Taught Programmes of Study.