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

Towards the end of the term we will be using the Spin tool (see Tutorial1) for describing and specifying safety critical systems. Spin and Xspin are installed on Prism (“spin” and “xspin” at the prompt).

• See course slides 01 and 02. There are 4 papers that are required readings for the next two weeks (01 to 04)

• 03 Slides on
  • Four descriptions of a system (D, R, S and M) and the formal justification that a specification S satisfies the requirements R in a problem domain D
  • UML Use Case Diagram and textual representation of a use case (UML Distilled Chapter 9, 3rd edition, 2004)
  • Jackson context diagrams (required readings: two articles in 05-Problem Frames, and chapter 2 of the Problem Frame book)

Assignment 1 due to be handed out next week

• 04 slides on
  • UML Statecharts
  • Problem Diagrams and Justifying the correctness of a specification