Course Outline

Notes for the course will be available from the SVN (usually updated at the end of the week, after the lectures for that week). Be sure to do all the Exercises in the Notes.

Notes. Questions. What is Software Engineering? What are Requirements? Is there a difference between Requirements & Specifications? The definition of Reliability. Products vs. Processes. The Waterfall Model, the V-model and CMMI.

Exercise: Do the mine pump exercise (Exercise 1) in Section 2.4 of the notes. Read the accompanying Teleologic Document (pages 15 and 16) on the anatomy of a good (atomic) requirement.

Required readings: AvL09 text, Chapter 1 (see SVN)

Slides 01 (up to #12): What is requirements engineering? The World and the Machine. The problem domain and solution domain. Requirements (R-descriptions), assumptions about the physical world (W-descriptions), Specifications (S-descriptions) and Programs (M-descriptions). Dependability arguments (validation and verification). Case study: Validation of requirements for a software controlled braking system.

Slides 02 (up to #85): Importance and structure of a requirements documents. Case study: bridge controller (requirements document, initial model for requirement FUN-2 in Event-B, proof obligations for requirement FUN-2, using the model to detect missing requirement FUN-4).

Exercise:

• (Exercise 3) Do all the exercises at the end of chapter 1 of AvL09.
• (Exercise 4) Line Editing Users Requirement Document
• Slides 01 (up to end). Error types in Requirements Documents such as contradictions, ambiguities, omissions etc. Various studies that show that a large proportion of errors in software development originate in the requirements or specification phase (late detection is costly to fix).
• Slides 03 (up to #32). What we are trying to achieve. What managers want to see. Overview of the big picture in the requirements process. Launching requirements elicitation/discovery. Using rich pictures. What are stakeholders? What are goals? Goal models. Difference between goals and requirements. Context diagrams and scope.

Exercises:

• (Exercise 5) Identify Problems in a Line Editing User's Requirements Document
• Exercises 6 and 7: UML Use Case and Sequence diagrams for requirements
• Slides 03 (to end): Requirements Discovery/Elicitation. Domain Knowledge. Identify Stakeholders/Views. Scenarios. UML Use Cases. UML sequence diagrams. Scenario driven search for exceptions. Reliability = Correctness + Robustness + Security. Handling Threats and Risks.

• Requirements Elicitation Session with Stakeholder for Project Phase1. Students must have thought about the required domain knowledge. Results of the elicitation meeting posted in the SVN.
• UML Class Diagrams. Class diagrams and mathematical contracts describe domain knowledge. We use the the dPost example to illustrate the ideas. Class invariants capture invalid/inconsistent input data and can thus be used as the basis for dealing with requirements exceptions (see 02 slides). Preconditions and postconditions can be used to define the required mathematical calculations in a precise and concise way. Note that we are developing a model of the problem domain (not of the solution/machine).

Test1 (Tuesday October 20th in CC 208, Calumet College, 4pm). Material covered in class up to last week (see all items above), required readings, Exercises, slides. Test1 is closed book but you may bring a single data sheet (letter size).

Lecture: (Thursday October 22 in CC 208): Guest lecture on Goal Models (i* and KAOS) by Jennifer Horkoff and Golnaz Elahi (working with Prof. Eric Yu) of the University of Toronto. See 04 slides. Why goal oriented requirements engineering? i* SD diagrams. i* SR diagrams. In class exercise using i* to model “greening” of ICSE conference. Model analysis and trade-offs. Comparsion with KAOS (as in the suggested text). Suggested background reading on KAOS: AvL09, chapter 7 and chapter 15 (for the mine pump system)

• Review of Test 1
• Requirements for safety critical systems (05 slide series up to slide 39). Suggested background reading: AvL09 text: Chapter 17.
  • Models can be used to test requirements and specifications
  • Engineerimg models
  • UML statecharts (XOR and AND superstates). A transition has a condition (or guard), and event name and an action. Difference between a precondition (as a correctness condition) and a guard (as a wait condition).
  • Safety properties (nothing bad must happen). Liveness properties (something good should eventually happen). Deadlock. Livelock.
  • CSP, vending machines and deadlock
  • Using the PAT2 tool for CSP, safety and liveness properties
  • The difference between testing and modelchecking
  • Using PAT2 to analyze the requirements for the bridge control.
  • Excercise for next week: develop a model for requirement R3: the bridge must be one-way (slide 39). Modelcheck the model for R3 and deadlock freedom. Simulate the model.

Tuesday's lecture: Series 5 slides continued, developing a PAT2 model for requirements of the bridge safety system. Initial Model. Limiting the number of cars on the island and bridge (requirement R2). First refinement: Introducing the one way bridge (requirement R3). Second refinement: introducing the traffic lights. This is the first model in which we can distinguish between W-descriptions and S-descriptions (the computer controller). From the analsysis we obtain a new liveness requirement. Verifying the safety and liveness requirements for the bridge safety system. Simulation of the model.

Thursday lecture: Reviewed the sample mathematical description for the time weighted return in Section 4.3 of the Phase project description. Showed how atomic requirements must be linked to the mathematical model and the mathematical model to the atomic requirements. By doing the mathematical model first, a better set of atomic requirements can be written.

Background reading for Thu. lecture: Section 4.4 in AvL09.

Exercises. Do Exercises 9, 10 and 11 in preperation for Test2 next week. See SVN/Exercises for the details. There will also be a question in the test on class-diagrams/mathematical-contracts (as required for Phase2).

Safety critical systems continued (till the end of series 05 slides).

• Decoupling the S-description from the W-description for the bridge controller. In PAT2, the W and S-descriptions are specified via CSP processes. The Requirements are described in linear time temporal logic (LTL). Checking the validity of the LTL requirements validates the specification (i.e. demonstrates the truth of W && S ⇒ R).
• What makes a good CSP specification? – for each input from the plant sensors , what is the output to the actuators. Disjointness and Completeness of input conditions of the Specification (as in Parnas tables, see later).
• Linear time temporal logic semantics. Henceforth, Eventually. Until. Expressing weak and strong fairness in LTL.
• The Train-Gate example in PAT2. The need for real-time constraints in the model. Clock = tick1 → tick2 → Clock. Shared events in CSP/statechart proecsses. The Train-Gate example (provided in SVN) can be used in the mine safety example (Excercise 11). Work through the train gate example in preparation for Tuesday's lecture.