Differences

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

--- course_outline [2011/11/22 19:24] – jonathan
+++ course_outline [2011/11/22 19:33] (current) – jonathan
@@ Line 96: / Line 96: @@
-**Thursday Nov 17**: Temporal Logic for stating requirements of reactive systems. Henceforth and Eventually operators and their formal semantics. Train-Gate with timing revisited: Need some notion of time to distinguish between "slow" and "fast" events. Introduction of explict clock ticks. Mechanical systems such as Train and Gate are "slow", i.e. there is a clock tick between state changes. Electronic systems such as the computer Controller ands the Light are "fast", i.e. can have multiple state changes between two ticks of the clock. See SVN for an explicit clock tick System with a random controller. **Exercise**: You must develop a controller that satisfies the safety and liveness requirements for next week.
+**Thursday Nov 17**: Temporal Logic for stating requirements of reactive systems. Henceforth and Eventually operators and their formal semantics. Train-Gate with timing revisited: Need some notion of time to distinguish between "slow" and "fast" events. Introduction of explict clock ticks. Mechanical systems such as Train and Gate are "slow", i.e. there is a clock tick between state changes. Electronic systems such as the computer Controller ands the Light are "fast", i.e. can have multiple state changes between two ticks of the clock. See SVN for an explicit clock tick System with a random controller. **Exercise**: You must develop a controller that satisfies the safety and liveness requirements for next week. (Hint: User a tabular expression (Parnas table) to specify the controller.
 **Required Reading**: [[https://wiki.cse.yorku.ca/course_archive/2011-12/F/4312/resources#pat_resources|CSP/PAT resources]]
+===== Week 12  =====
+**Tuesday Nov 22**: Fairness and Scheduling. Weak and Strong Event Fairness. Global Fairness. Lab: Solution to the Controller from last week.
+**Thursday Nov 25**: Introduction to Assignment 3: Bridge Controller. See [[http://www.event-b.org/A_ch2.pdf|Bridge System]] (Chapter 2 of Abrial book on Event-B) and [[http://deploy-eprints.ecs.soton.ac.uk/112/1/sld.ch2.car.pdf\slides]]. Assignment 3: What are Plant events and what are Controller events? Which are the measured variables and which are the controlled variables? Describe the Plant in PAT (E-descriptions). Write the R-descriptions in temporal logic. Specify the Controller in PAT so as to satisfy the requirements. Verify that the Controller satisfies the requirements.