User Tools

Site Tools


course_outline

Differences

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

Link to this comparison view

Both sides previous revisionPrevious revision
Next revision
Previous revision
course_outline [2009/11/12 23:45] jonathancourse_outline [2009/11/12 23:48] (current) jonathan
Line 72: Line 72:
 **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). **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.+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).    *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).   *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.   * 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. The Train-Gate example (provided in SVN) can be used in the mine safety example (Excercise 11 as well). Work through the train gate example in preparation for Tuesday's lecture.+  * 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.
course_outline.1258069546.txt.gz · Last modified: 2009/11/12 23:45 by jonathan

Donate Powered by PHP Valid HTML5 Valid CSS Driven by DokuWiki