Introductory Lecture. What are formal methods? Why formal methods? Our slides in class are taken from Chapter 1: Introduction.

Writing a user requirements document (URD). URD for the bridge controller. The initial Event-B model for the bridge controller (up to slide 33 of Chapter 2: Controlling cars on a bridge).

Required readings: Text Chapter I (pages 1-16). Text Chapter II (up to page 33)

First refinement of the bridge, i.e. up to slide 84 of “Controlling cars on a a bridge). We also had a lab on how to use the Rodin modelling tool to discharge invariant establishment, invariant preservation, and deadlock freedom proof obligations. Do Exercises on the SVN. Read the accompanying material in Ch II.

Up to (but not including) divergence of new events in the 2nd refinement.