State-Based Modelling

The Software Engineering Mathematics course introduces a means of describing and reasoning about formal descriptions of systems. In this course, we build upon those foundations to show how we might describe, animate and prove properties of state-based models in the languages of Z and B.

Frequency

This course normally runs once a year.

Course dates

Objectives

At the end of the course, students will be able to write and analyse state-based descriptions in terms of both the schema language of Z and the B-method. Students will be able to map from the so-called whiteboard approach of the former to the more tool-oriented approach of the latter.

Contents

The course will cover four broad topics: the schema language of Z; the B-method; analysing state-based descriptions via animation and model checking; and data refinement.

Assessment Criteria

• Have you demonstrated competence in the theory that underpins Z and B?
• Have you demonstrated competence in the application of the schema language of Z?
• Does your model offer a plausible interpretation of the problem as stated and is it appropriately structured?
• Are you able to navigate from a Z representation to a B representation?
• Have you demonstrated an understanding of the relevance of state-based modelling to the wider software engineering context?

Requirements

Attending an instance of the Software Engineering Mathematics course before registering for this course is strongly encouraged.