Differences

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

--- start [2012/12/23 01:27] – jonathan
+++ start [2013/03/20 14:52] (current) – jonathan
@@ Line 1: / Line 1: @@
 ~~NOTOC~~
-====== System Specification and Refinement  ======
+====== CSE3342 System Specification and Refinement  ======
@@ Line 7: / Line 7: @@
 ===== Lecture Times =====
-  *
+  * CSE3342 System Specification and Refinement, TR 11.30am, CB115. LAB Tuesday 13:00 LAS 1002A
-===== Description  =====
+  * **Important**: Subscribe to: [[https://forum.cse.yorku.ca/viewforum.php?f=201|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.
+  *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 also available at [[[[protected:project:labs|Labs]].
+  *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.
+  * Office hours: Monday 5.30-6.30pm and Thursdays 1pm-1.45pm in the SEL (CSE2056).
+===== Calendar Description  =====
 Theory and tools for specifying computer systems (sequential, concurrent and embedded). Specification (via set theory and predicate logic), modelling, abstraction, refinement and formal reasoning are undertaken before code development so that systems are correct by construction under the stated assumptions.
@@ Line 30: / Line 40: @@
   *Compare the theory with classical Hoare Logic and the Dijkstra weakest precondition calculus .
-Chapters 1, 2, 3, 4, 5 and 9 from the text Modeling in Event-B: System and Software Engineering, Jean-Raymond Abrial (Cambridge, to appear 2010) makes this a possible textbook for the course.
+Chapters 1, 2, 3, 4, 5, 9 and 15 from the text [[http://www.event-b.org/abook.html|Modeling in Event-B: System and Software Engineering]], Jean-Raymond Abrial (Cambridge) makes this a possible textbook for the course.
+This course is 3 hours of instruction per week as well as 1 hour of supervised labs per week.
+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.