start
Differences
This shows you the differences between two versions of the page.
Both sides previous revisionPrevious revisionNext revision | Previous revisionNext revisionBoth sides next revision | ||
start [2016/01/04 18:37] – jonathan | start [2016/04/19 22:16] – jonathan | ||
---|---|---|---|
Line 8: | Line 8: | ||
* EECS3342 System Specification and Refinement Lecture Times: | * EECS3342 System Specification and Refinement Lecture Times: | ||
- | * Class TR 11.30am, PSE321. <hi>Please check this page before the lecture as we may change the classroom to to the Bergeron Centre</ | + | * Class TR 11.30am, PSE321. <hi>Starting Thursday Jan 7, classes will be in the Bergeron Centre |
- | * **Scheduled Labs**: Every Tuesday | + | * **Scheduled Labs**: Every Tuesday |
+ | * In the Lab, we now use Rodin 3.2. | ||
* **Important**: | * **Important**: | ||
Line 15: | Line 16: | ||
*See bottom** ↓** of this page for login with your Prism password. Slides are available from the SVN repository (see link in the sidebar, once you have logged on). | *See bottom** ↓** of this page for login with your Prism password. Slides are available from the SVN repository (see link in the sidebar, once you have logged on). | ||
- | * The Labs to be done each week are available at [[[[protected: | + | * Instructions for the Labs will be provided |
*Read the course outline regularly. | *Read the course outline regularly. | ||
Line 22: | Line 23: | ||
* Suggested Text: Jean-Raymond Abrial, //Modeling in Event-B: System and | * Suggested Text: Jean-Raymond Abrial, //Modeling in Event-B: System and | ||
- | Software Engineering//, | + | Software Engineering//, |
+ | |||
+ | * See [[https:// | ||
===== Calendar Description | ===== Calendar Description | ||
Line 52: | Line 55: | ||
The lab time is used to give students detailed exercises and instruction in using a practical verification tool (such as Rodin for Event-B) to accompany the material in the lectures. Tools are essential to using the theory and methods on larger examples and require expert knowledge of the use of automated theorem proving methods. Students will use such tools to prove the examples that are discussed in class as well as larger examples. | The lab time is used to give students detailed exercises and instruction in using a practical verification tool (such as Rodin for Event-B) to accompany the material in the lectures. Tools are essential to using the theory and methods on larger examples and require expert knowledge of the use of automated theorem proving methods. Students will use such tools to prove the examples that are discussed in class as well as larger examples. | ||
+ | |||
+ | |||
+ | ==== Course Outline ==== | ||
+ | |||
+ | 1. High-level state/event models and proof rules for invariant preservation | ||
+ | 2. Refining a system and proving that the refinement preserves correctness | ||
+ | 3. Proving convergence and absence of deadlock | ||
+ | 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 | ||
+ | 6. Anticipated events in high-level models for convergence | ||
+ | 7. Use of contexts to develop relevant theories such as parity | ||
+ | 8. Nondeterministic systems and associated safety invariant proof 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 | ||
+ | 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 | ||
+ |
start.txt · Last modified: 2016/04/19 22:22 by jonathan