The course outline is a guideline to topics that will be discussed in the course, and when they will be discussed:

* Read the Rodin Users handbook up to and including Section 2.5.2.

• Bridge controller (reactive systems) Chapter 2: Controlling cars on a bridge).
  • Required readings: Read Chapters 1 and 2 from the suggested text chapter 2

Topics covered by the bridge controller include

• Initial models and Proof rules for invariant preservation
• Refinement/correct by construction
• Proof rules for refinement
• Deadlock prevention and relative deadlock
• Divergence, Convergent events and variants
• Proof rules including SIM
• Controller events and Environment events