Differences

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

--- course_outline [2009/10/30 20:07] – jonathan
+++ course_outline [2009/11/12 23:48] (current) – jonathan
@@ Line 44: / Line 44: @@
 **Test1** (Tuesday October 20th in CC 208, Calumet College, 4pm). Material covered in class up to last week (see all items above), required readings, Exercises, slides. Test1 is closed book but you may bring a single data sheet (letter size).
-**Lecture**: (Thursday October 22 in CC 208): Guest lecture on Goal Models (i* and KAOS) by Jennifer Horkoff and Golnaz Elahi (working with Prof. Eric Yu) of the University of Toronto. See 04 slides. Why goal oriented requirements engineering? i* SD diagrams. i* SR diagrams. In class exercise using i* to model "greening" of ICSE conference. Model analysis and trade-offs. Comparsion with KAOS (as in the suggested text).
+**Lecture**: (Thursday October 22 in CC 208): Guest lecture on Goal Models (i* and KAOS) by Jennifer Horkoff and Golnaz Elahi (working with Prof. Eric Yu) of the University of Toronto. See 04 slides. Why goal oriented requirements engineering? i* SD diagrams. i* SR diagrams. In class exercise using i* to model "greening" of ICSE conference. Model analysis and trade-offs. Comparsion with KAOS (as in the suggested text). Suggested background reading on KAOS: AvL09, chapter 7 and chapter 15 (for the mine pump system)
 ===== Week of October 26th=====
   * Review of Test 1
-  * Requirements for safety critical systems (05 slide series). Suggested background reading: AvL09 text: Chapter 17.
+  * Requirements for safety critical systems (05 slide series up to slide 39). Suggested background reading: AvL09 text: Chapter 17.
     * Models can be used to test requirements and specifications
     * Engineerimg models
-    * UML statecharts (XOR and AND superstates). A transition has a condition (or condition), and event name and an action.
+    * UML statecharts (XOR and AND superstates). A transition has a condition (or guard), and event name and an action. Difference between a precondition (as a correctness condition) and a guard (as a wait condition).
-    * Safety properties (nothing bad must happen). Liveness properties (something good should eventually happen. Deadlock. Livelock.
+    * Safety properties (nothing bad must happen). Liveness properties (something good should eventually happen). Deadlock. Livelock.
     * CSP, vending machines and deadlock
     * Using the PAT2 tool for CSP, safety and liveness properties
-    * Using PAT2 to analyze the requirements for the bridge control. For next week develop a model for requirement R3: the bridge must be one way (slide 39)
+    * The difference between **testing** and **modelchecking**
+    * Using PAT2 to analyze the requirements for the bridge control.
+    *** Excercise for next week**: develop a model for requirement R3: the bridge must be one-way (slide 39). **Modelcheck** the model for R3 and deadlock freedom. Simulate the model.
+===== Week of November 2nd=====
+**Tuesday's lecture**: Series 5 slides continued, developing a PAT2 model for requirements of the bridge safety system. Initial Model. Limiting the number of cars on the island and bridge (requirement R2). First refinement: Introducing the one way bridge (requirement R3). Second refinement: introducing the traffic lights. This is the first model in which we can distinguish between W-descriptions and S-descriptions (the computer controller). From the analsysis we obtain a new liveness requirement. Verifying the safety and liveness requirements for the bridge safety system. Simulation of the model.
+**Thursday lecture**: Reviewed the sample mathematical description for the time weighted return in Section 4.3 of the Phase project description. Showed how atomic requirements must be linked to the mathematical model and the mathematical model to the atomic requirements. By doing the mathematical model first, a better set of atomic requirements can be written.
+Background reading for Thu. lecture: Section 4.4 in AvL09.
+===== Week of November 9th =====
+**Exercises**. Do Exercises 9, 10 and 11 in preperation for Test2 next week.  See SVN/Exercises for the details. There will also be a question in the test on class-diagrams/mathematical-contracts (as required for Phase2).
+Safety critical systems continued (till the end of series 05 slides).
+  *Decoupling the S-description from the W-description for the bridge controller. In PAT2, the W and S-descriptions are specified via CSP processes. The Requirements are described in linear time temporal logic (LTL). Checking the  validity of the LTL requirements validates the specification (i.e. demonstrates the truth of W && S => R).
+  *What makes a good CSP specification? -- for each input from the plant sensors , what is the output to the actuators. Disjointness and Completeness of input conditions of the Specification (as in Parnas tables, see later).
+  * Linear time temporal logic semantics. Henceforth, Eventually. Until. Expressing weak and strong fairness in LTL.
+  * The Train-Gate example in PAT2. The need for real-time constraints in the model. Clock = tick1 -> tick2 -> Clock. Shared events in CSP/statechart proecsses. The Train-Gate example (provided in SVN) can be used in the mine safety example (Excercise 11). Work through the train gate example in preparation for Tuesday's lecture.