Specification and Design

This course shows how mathematics can be used to structure and reason about real 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, and how to verify that operations are properly defined.

An essential feature of the course is the workshop, in which students get the chance to develop their own specifications under expert supervision.

Course dates

Objectives

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, and reason about the robustness of a design.

Contents

Schemas:

overview of the schema language; patterns and structure; declarations and predicates; schema semantics; bindings and types.

Schema operators:

mechanisms for schema combination; abstract data types; state-based specification; encapsulation of data members; composition of operations.

Promotion:

structuring specifications; compositionality; parallel composition of components; replication; indexing and naming; object references.

Preconditions:

checking the consistency of specifications; calculating the applicability of operations; preconditions and data invariants; simplifying requirements.

Applications:

case studies and exercises, including: file system; bounded buffer; access control; connection-based protocols.

Requirements

The course assumes a working understanding of the mathematical language of Z, as taught in the Software Engineering Mathematics course. Software engineering mathematics is an ideal preparation.