Differences

This shows you the differences between two versions of the page.

--- course_outline [2009/12/14 20:15] – jonathan
+++ course_outline [2010/03/04 04:57] (current) – jonathan
@@ Line 2: / Line 2: @@
+===== Week 1: Jan 4 =====
-===== Week 1 =====
+Introductory Lecture. What are formal methods? Why formal methods? Our slides in class are taken from [[http://wiki.event-b.org/index.php/Event-B_Language|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 [[http://wiki.event-b.org/index.php/Event-B_Language|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).
+===== Week 2: Jan 11 =====
+Initial model of the bridge controller up to [[http://deploy-eprints.ecs.soton.ac.uk/112/1/sld.ch2.car.pdf|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.
+===== Week 3: Jan 18 =====
+Up to [[http://deploy-eprints.ecs.soton.ac.uk/112/1/sld.ch2.car.pdf|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 [[http://deploy-eprints.ecs.soton.ac.uk/112/1/sld.ch2.car.pdf|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).
+===== Week 4: Jan 25 =====
+Up to [[http://deploy-eprints.ecs.soton.ac.uk/112/1/sld.ch2.car.pdf|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 [[http://deploy-eprints.ecs.soton.ac.uk/112/1/sld.ch2.car.pdf|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.
+===== Week 5: Feb 1 =====
+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.
+===== Week 6: Feb 8 =====
+Finish up to and including 3rd refinement of ftp protocol [[http://deploy-eprints.ecs.soton.ac.uk/114/1/sld.ch4.file.pdf|slides]] from slide 44 to the end.
+**Required reading**: all of chapter IV
+===== Feb 15: reading week =====
+===== Week 9: Feb 22=====
+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).
+===== Week 9: March 1=====
+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).
+===== Week 10: March 8=====
+Complete the refinement/proof of the sort program.
+Dijkstra [[http://www.cs.utexas.edu/users/EWD/ewd04xx/EWD472.PDF|guarded command language]] and proofs of loops via variants and invariants.
+Chapter XVI: Location access controller