Skip to main content Skip to navigation

Department of Computer Science

CS412 Formal Systems Development

CS412 15 CATS (7.5 ECTS) Term 1

Availability

Option - MEng CS and DM, MSc CS

Prerequisites

CS130, CS131, CS262 (or CS242)

Academic Aims

To study methods for designing, analysing and programming complex computing systems.

This module uses formal techniques to explore the specification, design and implementation of example computer systems. It will cover more advanced features of specification and introduce data and functional refinement, considering how a system design may be modified in a variety of practical ways. Refining the specification to code is an important step in the software life-cycle. This module presents both the theoretical basis for this and practical means of refinement from system specification to program code.

Learning Outcomes

At the end of the module the student should be able to:

  • Write formal specifications in one or more chosen notations.
  • Understand the principles of formal verification and weakest precondition and the rules for specification consistency.
  • Work with online tools to develop specifications; to generate and prove obligations for machines consistency and correctness of refinements; to refine specifications and develop code.

  • Understand the principles of refinement and the formal rules that apply. Be able to find loop variants and invariants and to verify loops.

Content

Revision of sets, relations, functions and sequences.

Revision of basic specification skills.

Introduction to development tool

  • Basic syntax
  • Introduction to the AMN approach
  • Examples and use of tool

Case studies

Data refinement

  • Refinement
  • Relations and nondeterminism
  • Simulations

Functional Refinement

Review of refinement concepts using the Guarded Command Language

Assignment

  • Logical constants
  • Sequential composition
  • Conditional statements
  • Iteration

Implementation through refinement

Throughout the module there will be an emphasis on mathematics principles, tool support and the application of techniques in domains such as computer secuity and computational modelling.

Speakers from industry on the application of formal systems development, inclduing relevant case studies.

Books

  • Spivey JM, The Z Notation, Prentice Hall International Series in Computer Science, 1992.
  • Woodcock J and Davies J, Using Z: Specification, Refinement and Proof, Prentice Hall International Series in Computer Science, 1996.
  • Potter B, Sinclair J and Till D, An Introduction to Formal Specification and Z, Prentice Hall International Series in Computer Science, 1996.
  • Abrial J-R, The B Book, Cambridge University Press, 1996.
  • Schneider S, The B Method: An Introduction, Palgrave, 2001.
  • Hayes I, Specification Case Studies, Prentice Hall International Series in Computer Science, 1993.
  • Gries D, The Science of Programming, Springer-Verlag 1981.
  • Morgan CC, Programming from Specifications, Prentice Hall International Series in Computer Science, 1990.

Assessment

Two hour examination (60%), laboratories and coursework (40%)

Teaching

20 one-hour lectures plus 10 two-hour workshops