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

Thu. Sep 8: Slides 01: Introduction to requirements engineering. Solving the right problem (the one our customer needs to solve). Why “waste time” doing requirements? (i.e. the importance of RE).

Required readings: Chapter 1 of suggested text (AvL09)

Tuesday Sep. 13: Slides 02: Problem Domain vs. Solution Domain. Scope of RE. Requirements are about phenomena external to teh machine. E-descriptions, R-descriptions, S-descriptions, M-descriptions. Difference between a requirements and a Specification. Dependability/Certification argument. System-as-is vs. System-to-be. WHY, WHAT, WHO? Parnas 4-variable model.

Thu Sep 15: Functional vs. non-functional requirements. Omisions, Contradictions, Inadequqacie, Ambiguities etc. in Requirements Documents.

Required reading: How to write requirements (Telelogic)

Tuesday Sep 20: Mathematical Preliminaries for set theory and predicate logic (see SVN). Requirements Document (RD) first page, revision history, table of contents and figures, Vision statement/Goals (from requirements elicitation), Context Diagrams, Analysis of goals.

Thu. Sep 22: RD dictionary/glossary, E-statements and R-statements. We are studying a sample requirements document handed out in class (ROI-RD). We did the vision/goals statement, context diagram, analysis and dictionary/glossary explaing why each of these were needed. We also studied the actual atomic requirements documented as E-descriptions and R-descriptions.

Required readings: Mathematical Review.pdf amd Abrial2009-FaultlessSystems.pdf in the SVN

Tuesday Sep. 27: In the ROI-RD, we will study the mathematical model to see why it is needed to make the R-statements precise and testable. The mathematical model in this case is done via contracts in predicate logic/set-theory. In the past, contacts were used to describe machine phenomena, but there is nothing to stop us from using contracts to describe R-phenomena (i.e. in the world external to the machine).

Thu. Sep 29th: Please view the video by Michael Jackson, Engineering and Software Engineering presented at FOSE-2010. The slides are also available at the above site and on the SVN. Some questions

• Where was the term “software crisis” first used. What did it mean?
• What engineering technique was missing in the Therac-25 failure (ans: named components)
• What is the definition of software engineering (ans: development of a reliable software system taking the environment as a given)
• What does M, W |= R mean? What are the four ways in which SE can fail?
• Consider the two requirements in a traffic system: (R1) “Provide overriding priority for pedestrian requests” and (R2) “Respond directly to earliest lift request first”. Are there any problems (see slide 16.

Required Reading: Four Dark Corners of Requirements Engineering, Pamela Zave and Michael Jackson (See SVN).

Tue. Oct. 04: Completed our study of the ROI-RD. The importance of the mathematical model as a testing oracle and predictor of input/output behaviour. The difference between transformationa systems and reactive systems. The Traceability matrix for validating E,M |= R. The two major deficiencies in the ROI-RD: (a) lack of non-fumctional requirements (e.g. performance) and (b) the lack of a completeness arguments. Parnas tables and completeness. The importance of the precondition and invariant to make a Parnas-style completeness argument. See CSE4312-F11-04-HowToWriteSoftReq.docx for summary.

Thu Oct 6: Parnas Tables: table format, disjointness and completeness. UML Use Case models. System Border, Use cases, Actors, Associations. Includes and extends relations. Textual documentation of a Use Case with sequence of normal and alternative events and pre and post conditions. There are some books in Steacie on reserve on UML and use cases. There is some nice material on UML here.

Required reading: David Lorge Parnas, Paul C. Clements. “A Rational Design Process: How and Why to Fake It”. IEEE Trans. Software Eng., 1986. Available from Steacie library (online).

Work on Assignment 2 and the Project.

Tuesday Oct 18: In class, we discuss various issues regarding the IEEE-181 pulse specification (that was part of Assignment 1 and continues in Assignment 2) including: the mathematical model, test cases, error cases, and precision. We again stress that we need a method to assess relative completeness of our requirements and we again recommend using Parnas tables to make such an argument in the RD.

Thursday Oct 20: View the video by David Parnas, Precise Documentation: the Key to Better Software presented at FOSE-2010. The slides are also available at the above site and the SVN. Bottom Line (from the talk):

• Producing no documentation gets you in trouble.
• Producing bad documentation might be worse.
• Producing good documentation:
  • will help you get the requirements right
  • will help you get interfaces right
  • will help you in your testing
  • will help you in maintenance and upgrades
  • will help you manage a product line effectively.

Challenge Question: Use an appropriate (mathematical) table to document the IEEE-181 specification. Be careful to note the monitored and controlled variables.

Tues 25th/ Thu 27th: Student presentations of their critique of the requirments documents produced by other teams.

Tues Nov 1: Reactive/safety-critical systems vs. transformational systems. How do we write requirements for reactive systems. UML statecharts: XOR and AND composition. Deterministic vs. non-deterministic behaviour. Difference between a state and an event. Statecharts (syntax) versus their reachability graphs and executions (semantics). Reachable states vs. non-reachable states. How, we could in principle, check a safety requirement such as train will never be on the level crossing when the gate is up using a reachability graph. Simple CSP and the stress on events as opposed to states. Using CSP as an alternative to UML statecharts.

Thu Nov 3:

• Short lecture on astronomy and a mathematical model for the calculation of sunset. Discussed the ratio die mathematical model in Calendrical Calculations. Key point: Not any old mathematical model will do, but simplicity and elegance will help with precise documentation. Another Key point: in requirements elicitation you may often have to learn about an unfamiliar domain (e.g. IEEE pulses of Astronomical phenomena like sunrise/sunset) and thus will have to consult with domain experts for the E-assumptions.
• Requirements elicitation for the Project.
• CSP non-deterministic choice operator. The notion of deadlock and its importance for safety requirements of reactive systems. Using PAT to describe reactive models, generate reachability graphs, check for deadlock and generate counterexamples (executions or traces of the system in the reachability graph that show how you can get from an initial state to a deadlock state).

Required: (1) Read chapters 1 and 2 of CSP by C.A.R. Hoare for examples and background to CSP. (2) Install PAT3 (also available under windows in Prism). (3) Convert the examples done in class as UML/statecharts into CSP/PAT3, eg. the telephone system. Generate reachability graphs and check for deadlock.

Tues Nov 7: Specifying mutual exclusion of critical resources and verifying the Peterson alogorithm for mutual exclusion. Safety properties vs. Liveness properties and expressing these requirements in Temporal Logic. Deadlock, Starvation and Fairness. Introduction to Temporal Logic for requirements of safety critical systems (see slides). Using CSP/PAT to calculate the reachability graph and verify properties of the Peterson algorithm. Why you need weak fairness schedulability asasumption for Peterson and what this means.

Required: Do the following exercise before Thursday's lecture. How would you model mutual exclusion via semaphores in PAT? Pay attention to atomicity. Verify safety, deadlockfree, and fairness requirements for mutual exclusion via semaphores.

Thu Nov 9: The Train-Gate system, machine and environment. E-desciptions and R-descriptions. In class lab: Given the description of the Plant = Train || Gate | Light in class, you must do the following. (a) Represent the Plant in CSP/PAT (i.e. translate the informal E-descriptions into a CSP mathematical model). (b) Write out the requirements (in temporal logic) for System = Plant || Controller. There are safety and liveness requirements. 3. Come up with the specification of the Controller (as a Parnas tabular expression). 4. Represent the specification (tabulular expression) in CSP/PAT. 5. Check that System satisfies the safety and liveness requirements. Complete this by next week Tuesday.

Tuesday Nov 15: Review of CSP/PAT syntax and Shared Events. Analysis of the “bad” Traing-Gate from previous week. Critical problem: Timing. Exercise to be done before Thursday's class: (1) As E-description 1, assume that mechanical devices such as the train and gate are “slower” i.e. there is at least one “tick” of time between state changes. Electronic events are “faster”, i.e. they change state without a tick of time passing. (2) Describe the Plant using assumption E1. (3) Design a controller as a Parnas table (tabular expression) and then insert into System= Plant || Controller. (3) Verify that your controller satisfies safety and liveness conditions.

Thursday Nov 17: Temporal Logic for stating requirements of reactive systems. Henceforth and Eventually operators and their formal semantics. Train-Gate with timing revisited: Need some notion of time to distinguish between “slow” and “fast” events. Introduction of explict clock ticks. Mechanical systems such as Train and Gate are “slow”, i.e. there is a clock tick between state changes. Electronic systems such as the computer Controller ands the Light are “fast”, i.e. can have multiple state changes between two ticks of the clock. See SVN for an explicit clock tick System with a random controller. Exercise: You must develop a controller that satisfies the safety and liveness requirements for next week. (Hint: User a tabular expression (Parnas table) to specify the controller.

Required Reading: CSP/PAT resources

Tuesday Nov 22: Fairness and Scheduling. Weak and Strong Event Fairness. Global Fairness. Lab: Solution to the Controller from last week.

Thursday Nov 25: Introduction to Assignment 3: Bridge Controller. See Bridge System (Chapter 2 of Abrial book on Event-B) and http://deploy-eprints.ecs.soton.ac.uk/112/1/sld.ch2.car.pdf\slides. Assignment 3: What are Plant events and what are Controller events? Which are the measured variables and which are the controlled variables? Describe the Plant in PAT (E-descriptions). Write the R-descriptions in temporal logic. Specify the Controller in PAT so as to satisfy the requirements. Verify that the Controller satisfies the requirements.