Course Outline

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 demo, and Tutorial1) for describing and specifying safety critical systems. Spin and Xspin are installed on Prism (“spin” and “xspin” at the prompt).

On Prism, the SPIN tool is invoked by typing Xspin and the command line tool is spin.

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

• What are Requirements, how do they differ from Specifications?

• Formal and Informal Requirements.

• 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. This is in preparation for Project 3 which is to specify the requirements for a web application.
• [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.

• On Tuesday and Thursday there are two labs 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 doing requirements and specifications with SPIN.
• [10 series of slides] Tuesday's lecture is a continuation by Prof. Roumani on Web applications. This is in preparation for Project 3 which is to specify the requirements for a web application.
• [12 series of slides] Continuation of using SPIN for requirements and specifications of safety critical systems.

Slide series 10 on Object Oriented Modelling

Slide Series 11 on Object Oriented Modelling (Use Cases and Sequence Diagrams)

Slide Series 12. IEEE standards for Requirements Specifications. Natural language requirements vs. formal requirements.

Discussion of

Guest lectures by Prof. Alan Wassyng, McMaster University, on Parnas Tables and how Specifications were written for the Darlington nuclear reactor. Sliede series 13 and 14.