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)

• 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.

[Nov 24] Please make every effort to attend class next week as Prof. Wassyng is discussing important issues in requirements engineering. You may submit Project 1 up to Monday Dec. 3 noon without penalty. [Nov 20] On Nov 8 we noted that before you hand in Project 1, your team must understand the difference between the various industry standard (such as AIMR) investment return measures such as (X)IRR and TWR. We are running ouit of time on this one, so please hand in your two page description (see Nov 8 for details) in the assignment box by Thursday's class. Also, there will not be office hours today, but I will be in my office Wed. Nov 21 from 3-5pm if you want to come and talk to me about this issue. [Nov 20] Prof. Alan Wassyng is lecturing today on Parnas tables. [Nov 20] See correction to Excel sheet for TWR for Project 1. [Nov 14] Extra office hopurs today Nov 14, 1-2pm. [Nov 13] The test on Nov 15 is Closed Book. You mays bring one US-Letter size data sheet. If you miss the test: Notify the instructor immediately. You will need to provide an Attending Physicians statement (as on the York Registrar) site. Instructor must receive the Physician’s statement by November 20th. The makeup test will require you to use Spin in the SEL lab as a component of the test. [Nov 8] Assignment 3 submission details:what_you_must_submit [Nov 8] Changed all single ”&” in the Promela code of assignment 3 to ”&&”. [Nov 8] We are now using the new Forum instead of yahoo groups. Ask your questions about the Projects on this forum. [Nov 8] Assignment 2 grades now available. Read comments on calculating ROIs. Before you hand in Project 1, your team must understand the difference between the various industry standard (such as AIMR) investment return measures such as (X)IRR and TWR. The team must come to the instructor during office hours (or by appointment) with a two page description containing the following elements: Which precise industrial standard measure are you using and what is the reason you have chosen that measure. A precise description of how the calculation is done. Using the instructor's example scenario on the google spreadsheet, provide the instructor with how you will calculate the ROI using your description above. Using the instructor's example scenario on the google spreadsheet, provide the instructor with what you would have calculated using your description in assignment 2.