start
Differences
This shows you the differences between two versions of the page.
| Both sides previous revisionPrevious revisionNext revision | Previous revision | ||
| start [2016/04/19 22:16] – jonathan | start [2016/04/19 22:22] (current) – jonathan | ||
|---|---|---|---|
| Line 60: | Line 60: | ||
| 1. High-level state/event models and proof rules for invariant preservation | 1. High-level state/event models and proof rules for invariant preservation | ||
| + | |||
| 2. Refining a system and proving that the refinement preserves correctness | 2. Refining a system and proving that the refinement preserves correctness | ||
| + | |||
| 3. Proving convergence and absence of deadlock | 3. Proving convergence and absence of deadlock | ||
| + | |||
| 4. Overview of system modelling constructs and proof rules for correctness in a reactive system | 4. Overview of system modelling constructs and proof rules for correctness in a reactive system | ||
| + | |||
| 5. Design of a distributed systems illustrated with an ftp protocol | 5. Design of a distributed systems illustrated with an ftp protocol | ||
| + | |||
| 6. Anticipated events in high-level models for convergence | 6. Anticipated events in high-level models for convergence | ||
| + | |||
| 7. Use of contexts to develop relevant theories such as parity | 7. Use of contexts to develop relevant theories such as parity | ||
| + | |||
| 8. Nondeterministic systems and associated safety invariant proof rules | 8. Nondeterministic systems and associated safety invariant proof rules | ||
| + | |||
| 9. Design of sequential programs with correction by construction via refinement rules | 9. Design of sequential programs with correction by construction via refinement rules | ||
| + | |||
| 10. Hoare logic and weakest preconditions for program design and its use in a variety of developments | 10. Hoare logic and weakest preconditions for program design and its use in a variety of developments | ||
| + | |||
| 11. Methods for systematic development of correct-by-construction of reactive systems, illustrated with a train system | 11. Methods for systematic development of correct-by-construction of reactive systems, illustrated with a train system | ||
| + | |||
| 12. Thinking before Programming using Lamport’s TLA+ specification method | 12. Thinking before Programming using Lamport’s TLA+ specification method | ||
| + | ===== Grades ===== | ||
| + | |||
| + | * [30%] Weekly quizzes. There will be about 8 weekly quizzes (almost every week). The first 2 quizzes each count 3%. The last 6 quizzes each count 4%. On condition that the Lab work is completed. Quizzes will be based on the Labs, lectures and required readings of the preceding weeks. | ||
| + | * [15%] LabTest after reading week. | ||
| + | * [15%] Project (working in a team of no more than two students) | ||
| + | * [40%] Final exam | ||
| + | |||
| + | It is required that you attend and complete the work allocated in the weekly Lab session in preparation for the Quizzes, Labtest, Project and Exam. <hi> Labs must be completed by their due date in order for you to receive credit for the Quizzes</ | ||
start.1461104161.txt.gz · Last modified: 2016/04/19 22:16 by jonathan