====== EECS4312E-F19 ======

The tentative schedule for required readings (that you must do on your own), Scheduled Labs and Labtests are provided below. 

[[https://moodle.yorku.ca/moodle/course/view.php?id=162319|Moodle Site is here]]. Please register with iClicker for in class use. 

====== Schedule Fall 2019 ======

Tentative Labtest Dates & Required Reading

^Lab   ^Date          ^Labtest  ^Weight ^Weekly Required Readings^
| Lab00 | Wed. 04 Sep.|          |       |Slides-01: Requirements Overview|
| Lab01 | Wed. 11 Sep.|Labtest1  | 1%    |Section 2.1/2.2 Identify System Boundary|
| Lab02 | Wed. 18 Sep.|Labtest2  | 2%    |Section 2.3 Develop Operational Concepts|
| Lab03 | Wed. 25 Sep.|Labtest3  | 3%    |Section 2.4 Identify Environmental Assumptions|
| Lab04 | Wed. 02 Oct.|Labtest4  | 4%    |Section 2.5 Develop Functional Architecture|
| Lab05 | Wed. 09 Oct.|YK        |       |WIFT-PVS Prop. Logic p57-66|
|       | Wed. 16 Oct.|Reading W.|       |WIFT-PVS Pred. Logic p66-76|
| Lab06 | Wed. 23 Oct.|Labtest5  | 5%    |Section 2.6: Revise Architecture/Constraints|
| Lab07 | Wed. 30 Oct.|Labtest6  | 5%    |Section 2.7: Identify System Modes|
| Lab08 | Wed. 06 Nov.|Labtest7  | 5%    |Section 2.8: Detailed Behaviour/Performance|
| Lab09 | Wed. 13 Nov.|Project   | 20%   |Section 2.9/10: Define Software Requirements|
| Lab10 | Wed. 20 Nov.|Assignment| 10%   |Section 2.11: Provide Rationale|
| Lab11 | Wed. 27 Nov.|Exam Prep | 45%   ||
|       |             |          | 100%  ||


**You must be present in every laboratory during the scheduled Lab hour.** In most weeks, there will be a weekly Labtest during the scheduled Lab hour that is graded. The Labtest may cover all work done up to an including the previous week, including lectures, Labs and required readings. 

Every week there will be Lab work to be done (available on the SVN). See [[:protected:labs:start|here]]

Each week you are required to study readings, on your own time, during the course.
  * **Required text**: [[https://www.faa.gov/aircraft/air_cert/design_approvals/air_software/media/AR-08-32.pdf| Requirements Engineering Management Handbook (2009)]] (REMH). Note that there are examples of how to write requirements documents in Appendix A, B, C and D of this handbook. This allows you to see how the readings can be applied in practice. 
  * //WIFT-95 Tutorial Introduction to PVS// ([[https://wiki.eecs.yorku.ca/project/sel-students/p:tutorials:pvs:wift:start|WIFT-PVS Tutorial]]). Try out the examples using the PVS theorem prover. In addition, you must do the telephone book example in the WIFT-95 Tutorial (pages 5 to 25). 
  * You must also review UML (Use Case, Class, Statechart, Sequence Diagrams). There is a video to help you understand Use Cases. You must understand and be able to construct Use Cases and Use Case diagrams before the Project and Exam. See [[https://wiki.eecs.yorku.ca/course_archive/2017-18/F/4312/protected:videos:start#what_are_use_cases|here]].

As you attend the lectures, Labs and undertake the required readings note the various ways in which we **Elicit** and **Document** requirements including:
  * Informal prose descriptions
  * E/R descriptions
  * Use Cases, Statecharts and other UML diagrams
  * TLA+ Specifications
  * PVS Specifications especially completeness, disjointness and well-definedness of specifications
   * Acceptance Tests based on UI grammars, etc. 
   * A Requirements Document will involve a combination of carefully selected such methods. 

===== Topics Covered =====


  *Eliciting customer needs and goals and identifying the stakeholders.
  *The use of UML diagrams such as use case, sequence, class and statechart diagrams to help with the elicitation.
  *Developing the system overview, system boundary and context diagram.
  *Identifying the monitored variables and events and the controlled variables, their types ranges, precision and units.
  * Identifying the environmental assumptions and constraints.
  * Understanding the Parnas 4-variables model for writing requirements.
  * Monitored Variables, Controlled Variables, Timing resolution and Response Allowance
  *Developing the functional specification using tabular expressions (mathematical function tables)
  * The use of specification and theorem proving tools (PVS) to describe the function tables and using the PVS tool to verify the completeness, disjointness and well- definedness of the functional requirements.
  * PVS Specification of predicates using basic types, tuples, records, datatypes, functions, relations, sets, bags, etc. Reasoning about predicates in these types.
  * How to use function tables to specify safety-critical real-time systems and cyber-physical systems and understanding, Timing Resolution and Response Allowances.
  * Using function tables to specify business systems via monitored events and abstract states/controlled variables.
  *Validation of use cases against the functional specifications and validation of the safety requirements.
  *Describing non-functional and performance requirements.
  *Deriving acceptance tests from the use cases and function tables.

**Notes**: There are some slides available on the course web site but much of the work is done on the blackboard. Instruction in the use of PVS for specification and validation is done mainly via the Labs and the associated Labtests.