Formal Methods

Formal Methods explores specifying and constructing software systems so that they are correct by design. The module incorporates concepts of mathematical modelling, proof, formal specification, and programming for students to understand how to build safe, reliable software. Formal Methods begins by examining the place of formal methods in system and software design, before exploring the underpinning mathematics used in formal specification of computer systems. The module continues by examining how the underpinning mathematics is used to prove program correctness using standard techniques of preconditions and invariants. With these principles in place, students can explore a specific formal specification technique  the B-Method allowing students to specify a system based on its intended behaviour and correctness requirements. Finally, students will explore implementing their designs using a suitable programming language  Ada.

Formal Methods brings together concepts covered in Mathematics for Computer Science, the Software Development theme in computing programmes, and Software Architecture and Design. Formal Methods explores how the concepts developed in these prerequisite modules are augmented and combined to produce correct-by-design systems.

The aim of Formal Methods is to develop student's fluency in formal specification, application of mathematics in software design, and analytical skills using mathematical principles. The module capstones the software design and development areas of the programme, insofar that an understanding of software design and development is required to fully appreciate the need for formal specification. The module will require students to undertake evaluation of software requirements to understand safety issues and how to specify them. Doing so will best place students to understand the need to formally specify systems in safety critical conditions.