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 discharege invariant and deadlock freedom proof obligations. Do Exercises on the SVN.