Differences

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

--- course_outline [2009/11/10 19:52] – jonathan
+++ course_outline [2009/11/12 23:48] (current) – jonathan
@@ Line 70: / Line 70: @@
 ===== Week of November 9th =====
-**Exercises**. Do Exercises 9, 10 and 11 in preperation for Test2 next week. There will also be a question on class-diagrams/mathematical-contracts (as required for Phase2). See SVN/Exercises for the details.
+**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.