April 19, 2017 Outline

Reading: Chapters from revised text §5.2.3–5.4

1. Using the model
   1. Define ssc-preserving, *-property-preserving, ds-property-preserving
   2. Define relation W(ω)
   3. Show conditions under which rules are ssc-preserving, *-property-preserving, ds-property-preserving
   4. Show when adding a state preserves those properties
   5. Example instantiation: get-read for Multics
2. Tranquility
   1. Strong tranquility
   2. Weak tranquility
3. System Z and the controversy