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

Why testing alone is insufficient (example from quadratic equations).

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: 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: For the Labtests, you will be using Rodin under Linux. Do questions 1 and 2 (see EventB-Questions.pdf in the SVN). Note that any of the exercise questions may appear on the Labtest. For the Labtests, you will be using Rodin under Linux.

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.

in class we finished 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). Note that any of the exercise questions may appear on the Labtest. For the Labtests, you will be using Rodin under Linux. Also, use Rodin to prove the bridge controller up to the second refinement (done in in class).

Required Readings: Textbook, the whole of Chapter II (i.e. finish the bridge controller on your own).

This week we start Chapter IV of the textbook – A simple File Transfer Protocol (FTP). slides. 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). Note that any of the exercise questions may appear on the Labtest. For the Labtests, you will be using Rodin under Linux. 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.

Tuesday: First and second refinements of Chapter IV of the textbook – A simple File Transfer Protocol (FTP). slides. We also use sets and functions to model a banking system using Rodin (in class).

Thursday: Labtest1 (In preparation, do exercises 1-8).

Work on Assignment 2

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

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.

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).

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

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

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

Exercises: Do exercise 12 (birthday book, data refinement, procedural refinement).

Injections, surjections and bijections in Event-B.

Requirements for the sorting algorithm. Initial specification using an anticipated event. First and second refinements leading to the use of merge rules for a loop within a loop. For the slides see Sequential Programs.

Tuesday: Data refinement and Procedural Refinement. Illustration of these concepts using the Birthday Book example in which we write an initial specification, do a data refinement, followed by a procedural refinement; finally a merge produces code.

Thursday: Labtest2

Tuesday: Dijkstra weakest precondition calculus and loop variants and invariants.Proving loop termination. Relationship of Dijkstra weakest precondition calculus to Event-B. Slides on the SVN.

Thursday: Review of arithmetic, set theory, predicate logic and Event-B invariant and refinement proof obligations. Translation between set theoretic statements and predicate logic. Re-write rules.

Work through a complete example: requirements document, initial specification, refinements etc.