Differences

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

--- course_outline [2007/09/18 22:45] – jonathan
+++ course_outline [2008/06/25 21:23] (current) – jonathan
@@ Line 1: / Line 1: @@
 ====== Course Outline ======
+===== SPIN Tool =====
 The course outline is a guideline to topics that will be discussed in the course, and when they will be discussed.
-Towards the end of the term we will be using the [[http://spinroot.com/|Spin tool]] (see [[http://spinroot.com/spin/Doc/SpinTutorial.pdf|Tutorial1]]) for describing and specifying safety critical systems. Spin and Xspin are installed on Prism ("spin" and "xspin" at the prompt).
+Towards the end of the term we will be using the [[http://spinroot.com/|Spin tool]] (see [[https://www.cse.yorku.ca/~sel/4312/pub/readings/08-PROMELA-SPIN-tutorial1.swf|demo]], and [[http://spinroot.com/spin/Doc/SpinTutorial.pdf|Tutorial1]]) for describing and specifying safety critical systems. Spin and Xspin are installed on Prism ("spin" and "xspin" at the prompt).
+On Prism, the SPIN tool is invoked by typing //Xspin// and the command line tool is //spin//.
@@ Line 13: / Line 16: @@
-===== Weeks 1=====
+===== Week 1 Sep. 6th =====
   * See course slides 01 and 02. There are 4 papers that are required readings for the next two weeks (01 to 04)
+  * What are Requirements, how do they differ from Specifications?
+  * Formal and Informal Requirements.
@@ Line 36: / Line 45: @@
     * Problem Diagrams and Justifying the correctness of a specification
+===== Week 4 Sep 25 =====
+  *05 slides on the User Guide as a Requirement Document
+    *Required Reading: article by Berry et. al. (2001)
+    *Eliciting Requirements
+  *Elicitation Exercise in Class for Assignment 2
+===== Week 5 October 2=====
+  * 06 and 07 slides on the Fit framework for testable requirements and specifications
+  * The use of mathematical model libraries for specifications
+  * Detailed example (e.g. the birthday book) provided in the zip file
+===== Week 6 October 9=====
+  * Detailed review of Assignment 1. Model solutions provided on the assignment board outside the software engineering library (CSEB2056).
+  * D-descriptions and R-descriptions as statecharts. R-descriptions as mathematical invariants. Executing the statechart to verify the requirements R.
+===== Week 7 October 16=====
+  * 08 slides on the formal mathematical requirements and specifications via the B-method.
+  * See readings for supplementary reading (not required, but will be useful in the next assignment)
+===== Week 8 October 23=====
+  * [09 series of slides] Tuesday's lecture was by Prof. Roumani on Web applications. You must write a small Perl CGI script before next Tuesday's lecture. This is in preparation for Project 3 which is to specify the requirements for a web application.
+  * [11 series of slides] Introduction to SPIN and demo. Next week Tuesday and Thursday will be tutorials in the Software Engineerling Lab (CSEB2056) from 5.45pm to 6.45pm. Come and login and the instructor will be available to help you with SPIN.
+===== Week 9 October 30=====
+  * On Tuesday and Thursday there are two labs in the Software Engineerling Lab (CSEB2056) from 5.45pm to 6.45pm. Come and login and the instructor will be available to help you with doing requirements and specifications with SPIN.
+  * [10 series of slides] Tuesday's lecture is a continuation by Prof. Roumani on Web applications. This is in preparation for Project 3 which is to specify the requirements for a web application.
+  * [12 series of slides] Continuation of using SPIN for requirements and specifications of safety critical systems.
+===== Week of November 6  =====
+Slide series 10 on Object Oriented Modelling
+Slide Series 11 on Object Oriented Modelling (Use Cases and Sequence Diagrams)
+===== Week of  November 12 =====
+Slide Series 12. IEEE standards for Requirements Specifications.
+Natural language requirements vs. formal requirements.
+Discussion of
+===== Weeks of November 19 and 26 =====
+Guest lectures by Prof. Alan Wassyng, McMaster University, on Parnas Tables and how Specifications were written for the Darlington nuclear reactor. Sliede series 13 and 14.