This module is offered in 2020-21.


The aims of this module are:

  • To introduce the idea and motivation behind formal methods in general and model checking in particular.
  • To introduce the idea of program semantics and verification.

Learning Outcomes

On successful completion of this module, the student should:

  • Be aware of the need for formal methods and software verification.
  • Be familiar with a variety of well known model checkers.
  • Have a working knowledge of relevant approaches to modelling and property specification.
  • Understand the fundamental principles underlying model checking.
  • Be able to use transition systems as a model for systems, and temporal logics to express system properties including functional correctness, reachability, safety, liveness, fairness and real-time properties.
  • Be able to specify and verify models using various approaches including PROMELA and SPIN, timed Automata and UPPAAL (real-time systems), and Petri nets.


  • Modelling concurrent systems: transition systems, program graphs, parallelism and communication.
  • Linear-time properties: deadlock, safety, liveness, fairness contraints.
  • Temporal logics: LTL and CTL.
  • Model checking with PROMELA and SPIN.
  • Model checking with Timed Automata and UPPAAL.
  • Petri nets.
  • Program verification.

Compulsory Elements

This module has no compulsory elements beyond those common to all modules (mark of 4 in each assessment component).

Module Delivery

Back to top

Last Published: 19 Oct 2020.