course_outline
Differences
This shows you the differences between two versions of the page.
Both sides previous revisionPrevious revision | |||
course_outline [2009/11/12 23:47] – jonathan | course_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**. Do Exercises 9, 10 and 11 in preperation for Test2 next week. See SVN/ | ||
- | Safety critical systems continued. | + | Safety critical systems continued |
*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? | *What makes a good CSP specification? | ||
* 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 constraints in the model. Clock = tick1 -> tick2 -> Clock. Shared events in CSP/ | + | * The Train-Gate example in PAT2. The need for real-time constraints in the model. Clock = tick1 -> tick2 -> Clock. Shared events in CSP/ |
course_outline.1258069637.txt.gz · Last modified: 2009/11/12 23:47 by jonathan