University of Oxford Logo University of OxfordSoftware Engineering - Home
On Facebook
Follow us on twitter
Linked in
Linked in
Google plus
Google plus
Stumble Upon
Stumble Upon

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.


This course normally runs once a year.

Course dates

27th January 2025Oxford University Department of Computer Science - Held in the Department15 places remaining.


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.


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?


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