Differences

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

--- course_outline [2009/10/30 20:11] – jonathan
+++ course_outline [2009/11/12 23:48] (current) – jonathan
@@ Line 49: / Line 49: @@
   * 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
@@ Line 56: / Line 56: @@
     * CSP, vending machines and deadlock
     * Using the PAT2 tool for CSP, safety and liveness properties
+    * 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)
+    *** 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.