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: Controllong cars on a bridge).

Required readings: Textbook, Chapter I (pages 1-16). Textbook, Chapter II (up to page 33). Note that Chapters I and II are available as pdf (see textbook link).

Initial model of the bridge controller up to slide 68 of “Controlling cars on a a bridge. We also had a lab on how to use the Rodin modelling tool to discharge invariant establishmen and invariant preservation proof obligations. Do Exercises on the SVN. Read the accompanying material in Ch II.

Up to slide 82 of “Controlling cars on a a bridge”: We completes the initial model of the bridge controller for requirement FUN-2 (limiting cars on the bridge). We also discover the need for a new requirement (omitted in the original requirements document) for deadlock freedom – this is an optional proof obligation. Additional topics: before-after predicates, sequents, Peano arithemtic, proof obligations. In the Rodin tool: the difference between a context and a machine.

Up to slide 92: The next step is the notion of refinement (i.e. developing a concrete model closer to implementation from the abstract initial model). The refinement introduces new concrete variables and new events for requirement FUN-3 (the bridge must be one way). The refinement also introduces the notion of a glueing invariant.

Required reading from the textbook: Page 1-24 (Chapter II, Controlling cars on a bridge)

Required Exercises: Do questions 1 and 2 (see EventB-Questions.pdf in the SVN).

Up to slide 155 of “Controlling cars on a a bridge”: The proof obligations for a concrete event to refine an abstract event. The proof obligations on new events – they must refine 'skip”. New events must be shown not to diverge – thus requiring the notion of a variant. There are two proof obligations for a variant: a variant is a natural mumber expression; taking a new concrete event results in a value for the variant in the post-state less than it was in the pre-state.

Up to slide 214 of “Controlling cars on a a bridge”: Second refinement – introducing the traffic light. Two new variables for the traffic lights. Refining each of the abstract events ML_out and IL_out into two concrete events, and the need for a mutual exclusion condition (invariant) on the traffic light.

Required exercises this week (not for marks): Do questions 3, 4 and 5 in (see EventB-Questions.pdf in the SVN). Also, use Rodin to prove the bridge controller up to the second refinement (done in in class).

Required Readings: Textbook, Complete Chapter II on your own.

This week we do Chapter IV of the textbook – A simple File Transfer Protocol (FTP). There are exercises you must do to review and extend your knowledge of sets, functions and relations.

Required exercises this week (not for marks): Do questions 7, 8 and 9 in (see EventB-Questions.pdf in the SVN). Also, use Rodin to prove the bridge controller up to the second refinement (done in in class). Questions 8 and 9 will develop your ability to use functions and relations which is required for the rest of the course.

Finish up to and including 3rd refinement of ftp protocol slides from slide 44 to the end.

Required reading: all of chapter IV

Chapter XV: Development of sequential programs. Binary search. Merging Rules.

Celebrity example: Relations, functions, identity relation, inverse. Feasibility proof obligations for non-deterministic assignment, witness (WITH) for local variable refinements, convergence and proof obligations.

Use of Add Hypothesis (AH) and Case analysis (DC) in the theorem prover. Use RichPoor example.

Required reading: all of chapter IV and chapter V (Event-B proof obligation rules).

Exercises: Do exercise 11 (develop model, refinemenents and discharge proof obligations for ftp example).

Event refinement proof obligation (from Hallersted-Event-B-Notation-2006.pdf in the SVN).

How an anticipated event helps to specify termination.

Chapter XV: Development of sequential programs. Sort. Merging Rules.

Required reading: chapter XV as covered in class and all of chapter IX (Mathematical Language).

Complete the refinement/proof of the sort program.

Dijkstra guarded command language and proofs of loops via variants and invariants.

Chapter XVI: Location access controller