Differences

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

--- course_outline [2011/11/04 19:10] – jonathan
+++ course_outline [2011/11/22 19:33] (current) – jonathan
@@ Line 74: / Line 74: @@
 **Tues Nov 1**: Reactive/safety-critical systems vs. transformational systems. How do we write requirements for reactive systems. UML statecharts: XOR and AND composition. Deterministic vs. non-deterministic behaviour. Difference between a state and an event. Statecharts (syntax) versus their reachability graphs and executions (semantics). Reachable states vs. non-reachable states. How, we could in principle, check a safety requirement such as train will never be on the level crossing when the gate is up using a reachability graph. Simple CSP and the stress on events as opposed to states. Using CSP as an alternative to UML statecharts.
-**Thu Nov 3**: Short lecture on astronomy and a mathematical model for the calculation of sunset. Discussed the //ratio die// mathematical model in Calendrical Calculations. **Key point**: in requirements elicitation you may often have to learn about an unfamilar domain (here astronomy) and thus will have to consult with domain experts for the E-asumptiions.
+**Thu Nov 3**:
+  *Short lecture on astronomy and a mathematical model for the calculation of sunset. Discussed the //ratio die// mathematical model in Calendrical Calculations.  **Key point**: Not any old mathematical model will do, but simplicity and elegance will help with precise documentation. **Another Key point**: in requirements elicitation you may often have to learn about an unfamiliar domain (e.g. IEEE pulses of Astronomical phenomena like sunrise/sunset) and thus will have to consult with domain experts for the E-assumptions.
+  *Requirements elicitation for the Project.
+  *CSP non-deterministic choice operator. The notion of deadlock and its importance for safety requirements of reactive systems. Using PAT to describe reactive models, generate reachability graphs, check for deadlock and generate counterexamples (executions or traces of the system in the reachability graph that show how you can get from an initial state to a deadlock state).
-Requirements elicitation for the Project.
-CSP non-determistic choice operator. The notion of deadlock and its importance for safety requirements of reactive systems. Using PAT to describe reactive models, generate reachability graphs, check for deadlock and generate counterexamples (executions or traces of the system in the reachability graph that show how you can get from an inital state to a deadlock state).
+**Required**: (1) Read chapters 1 and 2 of [[http://www.usingcsp.com/cspbook.pdf|CSP]] by C.A.R. Hoare for examples and background to CSP. (2) Install [[http://www.comp.nus.edu.sg/~pat/|PAT3]] (also available under windows in Prism). (3) Convert the examples done in class as UML/statecharts into CSP/PAT3, eg. the telephone system. Generate reachability graphs and check for deadlock.
+===== Week 10  =====
-**Required**: (1) Read chapters 1 and 2 of [[http://www.usingcsp.com/cspbook.pdf|CSP]] by C.A.R. Hoare for examples and background to CSP. (2) Install [[http://www.comp.nus.edu.sg/~pat/|PAT3]] (also available under windows in Prism). (3) Convert the examples done in class as UML/statecharts into CSP/PAT3, eg. the telephone system. Gnerate reachability graphs and check for deadlock.
+**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.
-===== Week 10  =====
+**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  =====
-**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.
+**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.