Differences

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

--- start [2016/01/04 18:37] – jonathan
+++ start [2016/04/19 22:22] (current) – jonathan
@@ Line 8: / Line 8: @@
   * 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</hi>.
+    * Class TR 11.30am, PSE321. <hi>Starting Thursday Jan 7, classes will be in the Bergeron Centre BCE-213</hi>.
-    * **Scheduled Labs**: Every Tuesday 13:00 LAS 1002A. Labs attendance is required and there will be required labs, a quiz almost every week, and Labtests during some of the sessions.
+    * **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>
+    * In the Lab, we now use Rodin 3.2.
   * **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.
@@ 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).
-  * The Labs to be done each week are available at [[[[protected:labs|Labs]]. Lab0 must be completed in the first week of classes.
+  * Instructions for the Labs will be provided in the first lecture.
   *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.
@@ Line 22: / Line 23: @@
   * Suggested Text: Jean-Raymond Abrial, //Modeling in Event-B: System and
-Software Engineering//, Cambridge 2010. Available in Steacie. See SVN for notes. [[https://wiki.eecs.yorku.ca/project/sel-students/p:tutorials:eventb:start|Event-B Information]]
+Software Engineering//, Cambridge 2010. Available in Steacie. See SVN for notes.
+  * See [[https://wiki.eecs.yorku.ca/project/sel-students/p:tutorials:eventb:start|Event-B Information]] for notes on Equational Logic and also on the Sequent Calculus used by Event-B/Rodin. There is an online tutorial on the sequent calculus with point and click to try proofs. Rodin works somewhat differently but the underlying concepts are similar.
 ===== 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.
+==== Course Outline ====
+. High-level state/event models and proof rules for invariant preservation
+. Refining a system and proving that the refinement preserves correctness
+. Proving convergence and absence of deadlock
+. Overview of system modelling constructs and proof rules for correctness in a reactive system
+. Design of a distributed systems illustrated with an ftp protocol
+. Anticipated events in high-level models for convergence
+. Use of contexts to develop relevant theories such as parity
+. Nondeterministic systems and associated safety invariant proof rules
+. Design of sequential programs with correction by construction via refinement rules
+. Hoare logic and weakest preconditions for program design and its use in a variety of developments
+. Methods for systematic development of correct-by-construction of reactive systems, illustrated with a train system
+. 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>