Formal Specification

This course is studied in the second year of the BSc Computer Science course. It looks at using Formal Methods when designing systems in which dependability is a key issue. Formal methods use the mathematics of logic and set theory in system specification and the mathematics of proof theory in system validation and verification.

Overview

A Module Descriptor is available for this course. The topics covered are:-

Important Notice - In Order to view the following pages correctly you must have the Z-formaliser font installed on your system it is also recommended that you use Internet Explorer.

Online Course Material

This is some of the material used in the module. It includes the case studies looked at in lectures, solutions to the class tutorials and sample solutions to the exercises in the first part of the assignment.

Case Studies -

  1. Simple Security System
  2. Banking System
  3. Petrol Filling Station
  4. Therapy Machine

Solutions to Tutorials -

  1. Academic Administrator
  2. Filing Subsystem
  3. Weather Map
  4. Warehouse Stock Control

Sample Solutions to Assignment (part1)

Courseware : Formaliser

This is a software tool developed by a company called Logica. Its function is to assist software designers when specifying systems using the formal specification language Z. It provides an editor for entering/amending the specification; this includes a syntax parser. It also provides a facility for checking the specification with respect to the type and scope of information. his package is available to students studying this module. A user guide is provided.

Formaliser User Guide

Module List