====== Course Outline ====== ===== Week 1: Jan 4 ===== 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