EECS3342

User Tools

Site Tools

You are here: EECS3342 2017W System Specification and Refinement
Trace:
start

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revisionPrevious revision
Next revision		Previous revision
start [2016/04/19 22:16] – jonathanstart [2017/01/05 22:34] (current) – jonathan
Line 1: Line 1:
 ~~NOTOC~~ ~~NOTOC~~
-====== EECS3342 2016W System Specification and Refinement  ======+====== EECS3342 2017W System Specification and Refinement  ======
  
-EECS3342 **Winter 2016** Specification and Refinement+EECS3342 **Winter 2017** Specification and Refinement
  
 +[[https://www.youtube.com/watch?v=fSWZWXx5ixc|Video introducing Event-B/Rodin]] 
  
 ===== Getting Started ===== ===== Getting Started =====
  
   * EECS3342 System Specification and Refinement Lecture Times:   * EECS3342 System Specification and Refinement Lecture Times:
-    * Class TR 11.30am, PSE321. <hi>Starting Thursday Jan 7, classes will be in the Bergeron Centre BCE-213</hi>. +    * Class TR 11.30am <hi>From 10 January and onwards, lectures are in Bergeron 213</hi>.   
-    * **Scheduled Labs**: Every Tuesday 1pm to 2pm in LAS 1002A. Labs attendance is required and there will be required labs, and a quiz almost every week, and Labtests during some of the sessions. <hi> The first lab is due Tuesday Jan 12 by 1.30pm. Quiz 1 is 1.30pm to 1.55pm</hi> +    * **Scheduled Labs**: Every Tuesday 1pm to 2pm in LAS 1004. Labs attendance is required and there will be required labs, and a quiz almost every week, and Labtests during some of the sessions. <hi> The first lab is now available, and due Tuesday Jan 17 at 11am, and the first Quiz will be on Tuesday Jan 17th, during the Lab</hi> 
-    * In the Lab, we now use Rodin 3.2.+    * In the Lab, we now use Rodin 3.2. See [[:resources|Resources]]
  
-  * **Important**: Subscribe to: [[https://forum.cse.yorku.ca/viewforum.php?f=306|3342 Forum]] for the latest announcements. Please ask all questions relating to the course material on the forum (not via email). For all other questions, see me during office hours. +  * **Important**: Subscribe to the forum for the latest announcements. Please ask all questions relating to the course material on the forum (not via email). For all other questions, see me during office hours. 
  
   *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).
Line 20: Line 21:
   *Read the course outline regularly.  It is important to read all the required readings (not all of which are discussed in class). It is important to do the suggested exercises.   *Read the course outline regularly.  It is important to read all the required readings (not all of which are discussed in class). It is important to do the suggested exercises.
  
-  * 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 PDF for the [[https://www3.hhu.de/stups/handbook/rodin/current/html/|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   * Suggested Text: Jean-Raymond Abrial, //Modeling in Event-B: System and
Line 60: Line 61:
  
 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</hi> 
start.1461104161.txt.gz · Last modified: 2016/04/19 22:16 by jonathan