System Design and Refinement

Pre-requisite

Those of you considering taking this course should be aware that before the course commences you must go through Chapters 1-10 of Using Z (you should already know this material, but it's good revision), and also read more thoroughly Chapters 11-18. This reading is a pre-requisite to taking the course.

Aims

This course shows how mathematics can be used to structure and reason about information systems. It shows how the Z notation can be used to describe complex pieces of software in a clear and comprehensible fashion. It shows how to check a set of requirements for logical consistency, how to verify that operations are properly defined, and how to ensure that an implementation conforms to its specification by using the techniques of simulations.

Requirements

The course assumes a working knowledge of discrete mathematics. Introduction to Specification is ideal preparation.

Learning Outcomes

At the end of the course, students will be able to construct mathematical specifications of real systems. They will be able to check a set of requirements for consistency, reason about the robustness of a design, and confirm that one design refines another.