Differences

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

--- course_outline [2011/11/04 19:14] – jonathan
+++ course_outline [2011/11/22 19:33] (current) – jonathan
@@ Line 84: / Line 84: @@
 ===== Week 10  =====
-**Tues Nov 7**: Specifying mutual exclusion of critical resources and verifying the Peterson alogorithm for mutual exclusion. //Safety// properties vs. //Liveness// properties and expressing these requirements in Temporal Logic. Using Temporal Logic for requirements of safety critical systems. Example: Train-Gate system.
+**Tues Nov 7**: Specifying mutual exclusion of critical resources and verifying the Peterson alogorithm for mutual exclusion. //Safety// properties vs. //Liveness// properties and expressing these requirements in Temporal Logic. Deadlock, Starvation and Fairness. Introduction to Temporal Logic for requirements of safety critical systems (see slides). Using CSP/PAT to calculate the reachability graph and verify properties of the Peterson algorithm. Why you need weak fairness schedulability asasumption for Peterson and what this means.
+**Required**: Do the following exercise before Thursday's lecture. How would you model mutual exclusion via semaphores in PAT? Pay attention to atomicity. Verify safety, deadlockfree, and fairness requirements for mutual exclusion via semaphores.
+**Thu Nov 9**: The Train-Gate system, machine and environment. E-desciptions and R-descriptions. **In class lab**: Given the description of the Plant = Train || Gate | Light in class, you must do the following. (a) Represent the Plant in CSP/PAT (i.e. translate the informal E-descriptions into a CSP mathematical model). (b) Write out the requirements (in temporal logic) for System = Plant || Controller. There are safety and liveness requirements. 3. Come up with the specification of the Controller (as a Parnas tabular expression). 4. Represent the specification (tabulular expression) in CSP/PAT. 5. Check that System satisfies the safety and liveness requirements. Complete this by next week Tuesday.
+===== Week 11  =====
+**Tuesday Nov 15**: Review of CSP/PAT syntax and Shared Events. Analysis of the "bad" Traing-Gate from previous week. Critical problem: Timing. Exercise to be done before Thursday's class: (1) As E-description 1, assume that mechanical devices such as the train and gate are "slower" i.e. there is at least one "tick" of time between state changes. Electronic events are "faster", i.e. they change state without a tick of time passing. (2) Describe the Plant using assumption E1. (3) Design a controller as a Parnas table (tabular expression) and then insert into System= Plant || Controller. (3) Verify that your controller satisfies safety and liveness conditions.
+**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.