start
Differences
This shows you the differences between two versions of the page.
Both sides previous revisionPrevious revisionNext revision | Previous revision | ||
start [2014/12/29 18:24] – jonathan | start [2016/04/19 22:22] (current) – jonathan | ||
---|---|---|---|
Line 1: | Line 1: | ||
~~NOTOC~~ | ~~NOTOC~~ | ||
- | ====== EECS3342 | + | ====== EECS3342 |
+ | EECS3342 **Winter 2016** Specification and Refinement | ||
Line 8: | Line 8: | ||
* EECS3342 System Specification and Refinement Lecture Times: | * EECS3342 System Specification and Refinement Lecture Times: | ||
- | * Class TR 11.30am, | + | * Class TR 11.30am, |
- | * Every Tuesday | + | * **Scheduled Labs**: |
+ | * In the Lab, we now use Rodin 3.2. | ||
- | * **Important**: | + | * **Important**: |
*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 in the first lecture. |
*Read the course outline regularly. | *Read the course outline regularly. | ||
Line 21: | Line 22: | ||
* In the SVN → Docs, you will find the Rodin 2.8 Manual. Please familiarize yourselves with all the material in the manual, during the first week of classes. | * In the SVN → Docs, you will find the Rodin 2.8 Manual. Please familiarize yourselves with all the material in the manual, during the first week of classes. | ||
+ | * Suggested Text: Jean-Raymond Abrial, //Modeling in Event-B: System and | ||
+ | Software Engineering//, | ||
+ | |||
+ | * See [[https:// | ||
===== Calendar Description | ===== Calendar Description | ||
Line 32: | Line 37: | ||
After successful completion of the course, students are expected to be able to: | After successful completion of the course, students are expected to be able to: | ||
- | *Understand the nature of formal methods and evaluate their suitability. | + | |
- | *Understand user requirements | + | *Document |
- | *Construct high level, abstract mathematical models of a system (consisting of both the system and its environment) amenable to formal reasoning. | + | *Construct high level, abstract mathematical models of a system (consisting of both the system and its environment) amenable to formal reasoning. |
- | *Use set theory and predicate logic to express functional and safety properties from the requirements as events, guards, system variants and invariants of a state-event model. | + | *Apply set theory and predicate logic to express functional and safety properties from the requirements as events, guards, system variants and invariants of a state-event model. |
- | *Understand how to use models to reason about and predict their safety and liveness | + | *Use models to reason about and predict their safety and progress |
- | *Construct | + | *Plan and construct |
- | *Know the theory underlying state-event systems, refinements and their proof obligations. | + | *Prove |
*Apply the method to a variety of systems such as sequential, concurrent and embedded systems. | *Apply the method to a variety of systems such as sequential, concurrent and embedded systems. | ||
- | *Use practical tools for constructing and reasoning about the models. | + | *Use practical tools for constructing and reasoning about the models. |
- | *Compare the theory with classical | + | *Use Hoare Logic and Dijkstra weakest precondition calculus |
Chapters 1, 2, 3, 4, 5, 9 and 15 from the text [[http:// | Chapters 1, 2, 3, 4, 5, 9 and 15 from the text [[http:// | ||
Line 49: | 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 | ||
+ | |||
+ | ===== 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.txt · Last modified: 2016/04/19 22:22 by jonathan