course_outline
Differences
This shows you the differences between two versions of the page.
Both sides previous revisionPrevious revisionNext revision | Previous revision | ||
course_outline [2010/01/07 22:48] – jonathan | course_outline [2010/03/04 04:57] (current) – jonathan | ||
---|---|---|---|
Line 1: | Line 1: | ||
====== Course Outline ====== | ====== Course Outline ====== | ||
- | |||
Line 9: | Line 8: | ||
Writing a user requirements document (URD). | Writing a user requirements document (URD). | ||
- | **Required readings: | + | **Required readings: |
+ | |||
+ | |||
+ | |||
+ | |||
+ | ===== Week 2: Jan 11 ===== | ||
+ | |||
+ | Initial model of the bridge controller up to [[http:// | ||
+ | |||
+ | ===== Week 3: Jan 18 ===== | ||
+ | |||
+ | Up to [[http:// | ||
+ | |||
+ | Up to [[http:// | ||
+ | |||
+ | |||
+ | **Required reading from the textbook**: Page 1-24 (Chapter II, Controlling cars on a bridge) | ||
+ | |||
+ | **Required Exercises**: | ||
+ | |||
+ | ===== Week 4: Jan 25 ===== | ||
+ | |||
+ | Up to [[http:// | ||
+ | |||
+ | |||
+ | Up to [[http:// | ||
+ | |||
+ | **Required exercises this week** (not for marks): Do questions 3, 4 and 5 in (see // | ||
+ | |||
+ | **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 // | ||
+ | |||
+ | ===== Week 6: Feb 8 ===== | ||
+ | |||
+ | Finish up to and including 3rd refinement of ftp protocol [[http:// | ||
+ | |||
+ | **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, | ||
+ | |||
+ | 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**: | ||
+ | |||
+ | ===== 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/ | ||
+ | Dijkstra [[http:// | ||
+ | Chapter XVI: Location access controller |
course_outline.1262904512.txt.gz · Last modified: 2010/01/07 22:48 by jonathan