The schedule below (taken from Winter 2010) will be updated as the term proceeds.

The SVN will have a list of exercises that you must do on your own to test your knowledge of the material and to help you to prepare for the labtests and exam.

Background Readings

• What/Why formal methods? Slides Chap. 1: Introduction.
• Textbook Chapter I (pages 1-16).

Required:

• Slides MathsAndEngineering.pdf (from the SVN) Why testing alone is insufficient (example from quadratic equations).
• Chapter II (up to page 33). 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).

It's a good idea to get the Rodin 2.0.1 tool up and working on your Laptop (see Resources). Do Exercise 1.

Tuesday's lecture: We finished the initial model of the bridge controller and started on the the first refinement up to slide 89 of “Controlling cars on a a bridge. Exercise: In the initial model, enter DLF as an invariant (but set its status to theorem). Confirm that you are not able to prove it without the missing axiom. Then add the missing axiom and demonstrate DLF. Do the proofs in the Rodin tool as well as by hand. Usually, if you can do the proofs by hand then you can guide the tool to do the proofs as well (where it does not discharge automatically).

Thursday's lecture: We finished up to slide 129 of “Controlling cars on a a bridge. We discussed the notion of a concrete model refining an abstract model and the notion of event refinement including guard strengthening and the concrete event simulating the abstract event. The refinement proof obligations were discussed in detail.

We also had a lab on how to use the Rodin modelling tool to discharge invariant establishmen and invariant preservation proof obligations. We also saw how to use AnimB plugin. Do Exercises on the SVN. Read the accompanying material in Ch II.

Exercises: By the end of this week, complete Exercises 1, 2, and 3 (on the SVN) in preparation for the labtest. Make sure that on the Prism/Linux workstations you can generate PDf docs (via latex) and export projects as zip files.

Tuesday's lecture: We finished up to slide 155 of “Controlling cars on a a bridge. We continued the discussion of the notion of a concrete model refining an abstract model and the proof obligations. New events must refine skip and there are also proof obligations to ensure that the new events do not diverge. We also discussed the proof obligations for relative deadlock freedom (needed because guards in a refinement can be strengthened)

Thursday's lecture: Completed the second refinement with the traffic lights up to slide 239. We discussed the new proof rule SIM as well as splitting an event in the refinement. We showed how the proof obligations lead us to fix the model so that it works to specification. New invariants had to be introduced to prove the one way bridge requirmement. The new events for the traffic lights might diverge so new variables were introduced to ensure fairness.

Required readings: Read up to end of the second refinement of chapter 2 (p50) from the sample textbook.

Required Exercises: By the end of this week, you must have done Exercises 1-4.

Tuesday's lecture: Finished the third refinement of the bridge controller, i.e. we added the sensors so that the complete environment and controller are now in the model. We held a Laboratory session on Rodin in class to discuss Exercises 1-4 in preparation for the labtest. We imported and exported projects, used AnimB simulation plugin, generated Latex documentation, and did some manual theorem proving illustaring “dc” i.e. case split.

Thursday: Labtest 1

Required Readings: Textbook, the whole of Chapter II (i.e. finish the bridge controller on your own all the way up to to the end of the chapter).

This week we start Chapter 4 of the optional textbook – A simple File Transfer Protocol (FTP). In the previous example, the program was reactive (i.e. it had to control an external situation such as cars on a bridge). This chapter deals with a protocol used on a computer network to transfer data from a sender to a receiver. The example will also allow us to extend our mathematical language with sets, functions and relations. As usual we will start with a requirements document. The initial model tells us what the protocol is supposed to achieve without telling us how to achieve it; how to achieve it will be dealt with in succesive refinements. Note that the model presented in the slides (using the notion of an anticipated event) is different than that of the textbook.

Tuesday's lecture: We reviewed the 2nd refinement question in Labtest1. We also did ftp slides (up to slide 26). There are exercises you must do to review and extend your knowledge of sets, functions and relations.

Thursday's lecture: We reviewed the first refinement of the ftp protocol. We then had a lab session in which the initial model and refeinement were entered in Rodin and proved. We also did some predicate logic in the theorem prover (with the aut-tactics disabled).

Required exercises this week (not for marks): Do questions 5, 6, 7, 8 and 9 in EventB-Questions.pdf in the SVN.

Required Reading: See SVN (folder 04-ftp): Read 04-ftp.pdf and 05-eventb-notation.pdf.

Note: Labtest2 is on March 1. By that time you must finish up to and inluding questions 15 (celebrity.pdf) and 16 (ftp).

Tuesday's lecture: We did the second refinement in the ftp protocol in which we separate the sending and receiving agent. We had a lab session with Rodin, proving cross-products, powersets, relations and functions.

Thursday's lecture: Third and final refinement in the ftp protocol in which we add a parity bit. The distributed ftp protocol is now ready to be implemented in code (how would you write the program?) with a guarantee that it will terminate with the file properly transmitted from the sender to the receiver. Lab: prove the parity bit theorem.

Required Reading: In the SVN=⇒Rodin folder, study: ref-card.pdf

Tuesday's Lecture: Did a manual proof of the theorem needed for the theory of parity (in the ftp protocol). This theorem was hard to prove. The suggestion is to first do the proof manually, which then makes it easier to do in Rodin. Using this approach, we were able to derive a Lemma that was helpful in the Rodin proof. We also did the initial model of the celebrity example (from the Exercises). We showed how to formalize the problem in Event-B using a “knows” relation. We dicussed the indentity and inverse relations and showed how the Celebrity axioms could be written in predicate logic or set theory. The celebrity example is one of the exercises that you must do in advance of Labtest1. [Challenge: In class we issued the following challenge: write a program given that takes as input a set of people and a knows relation, and outputs which person is the celebrity.

Thursday's lecture: Chapter 15: Development of sequential programs. Binary search. Merging Rules.

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

Required reading: Chapter 15.

Exercises: Up to an including Exercise 16.

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.