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

• 05 slides on the User Guide as a Requirement Document
  • Required Reading: article by Berry et. al. (2001)
  • Eliciting Requirements
• Elicitation Exercise in Class for Assignment 2

• 06 and 07 slides on the Fit framework for testable requirements and specifications
• The use of mathematical model libraries for specifications
• Detailed example (e.g. the birthday book) provided in the zip file

• Detailed review of Assignment 1. Model solutions provided on the assignment board outside the software engineering library (CSEB2056).
• D-descriptions and R-descriptions as statecharts. R-descriptions as mathematical invariants. Executing the statechart to verify the requirements R.

• 08 slides on the formal mathematical requirements and specifications via the B-method.
• See readings for supplementary reading (not required, but will be useful in the next assignment)

• [09 series of slides] Tuesday's lecture was by Prof. Roumani on Web applications. You must write a small Perl CGI script before next Tuesday's lecture.
• [11 series of slides] Introduction to SPIN and demo. Next week Tuesday and Thursday will be tutorials in the Software Engineerling Lab (CSEB2056) from 5.45pm to 6.45pm. Come and login and the instructor will be available to help you with SPIN.

• Tuesday and Thursday provide tutorials in the Software Engineerling Lab (CSEB2056) from 5.45pm to 6.45pm. Come and login and the instructor will be available to help you with SPIN.
• [10 series of slides] Tuesday's lecture is a continuation by Prof. Roumani on Web applications.
• [12 series of slides] Introduction to SPIN and demo. Next week Tuesday and Thursday will be tutorials in the Software Engineerling Lab (CSEB2056) from 5.45pm to 6.45pm. Come and login and the instructor will be available to help you with SPIN.