EECS4312

This page is read only. You can view the source, but not change it. Ask your administrator if you think this is wrong.
====== Course Outline ======

The course outline is a guideline to topics that will be discussed in the course, and when they will be discussed. The PVS Quiz is always during the Tuesday Lecture based on the PVS Exercise and all lecture material of the previous week. There will be no make-up for Quizzes (students are thus advised to always attend the Tuesday lecture to avoid a zero grade).



===== Due Dates =====
**You must be in the Lab during the scheduled Lab hour. Expect to take quizzes during the Lab hour on the PVS work and readings in the required text REMH. Lab work must be submitted before the Quiz.**

{{:quiz-instructions.pdf|Quiz Instructions}}

  * Sep. 17 during lab: Quiz1 (based on Lab0 and readings and lectures of the first week). At the command line in your Prism account, you can check your grade for the quiz via: ''feedback 4312 quiz1''.✓ (3%)
  * Sep. 24 during Lab: Quiz2. You will receive a grade for Quiz2, only if you submit your completed Lab1 by 5.45pm (before the start of Quiz2 at 6.10pm).✓ (3%)
  * Oct 1 during Lab: Quiz3✓ (3%)
  * Oct 08 during Lab: Quiz4✓ (3%)
  * Oct 15 during Lab: Quiz5✓ (3%)
  * Oct 22 during Lab: Quiz6✓ (4%)
   *Nov 05 during Lab: Quiz7✓ (4%)
   *Nov 19 during Lab: Quiz87✓(4%)
   *Dec 03 during Lab: **[[http://www.eecs.yorku.ca/~sel/quiz/4312/quiz9|Quiz9]]** (3%)
  * Nov 13: Due date for Assignment (10%) 
  * Dec 07: Due Date for Project (20%)

===== TENTATIVE Schedule =====

Each week you are required to study readings, on you own time, from:
  * the //WIFT-95 Tutorial Introduction to PVS// ([[https://wiki.eecs.yorku.ca/project/sel-students/p:tutorials:pvs:|see PVS page]]). Try out all the examples in the PVS theorem prover.
  * the required text: //Requirements Engineering Management Handbook// (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. 

The labs, quizzes, assignment, project and exam will be based on your knowledge of the required reading/study material as well as material presented in class. 

<hi cyan> In addition, each Lab has some reading/preparation to do before the Lab.</hi>

^Week ^Date       ^Lab(Th) ^Quiz  ^Assigns ^Study WIFT-PVS/REMH)                       |
|1  | Thu 10 Sep | Lab0   |      |        | WIFT-PVS Prop. Logic pages 57-66           |
|2  | Tue 15 Sep | Lab1   | 1    |        | WIFT-PVS Pred. Logic pages 66-76           |     
|2  | Tue 22 Sep | Lab2   | 2    |        | WIFT-PVS Phone Book Specification p5-25    |  
|3  | Tue 29 Sep | Lab3   | 3    |        | Sect2:2 Identify System Boundary           |  
|4  | Tue 06 Oct | Lab4   | 4    |        | Sect2:3 Develop Operational Concepts       | 
|5  | Tue 13 Oct | Lab5   | 5    |        | Sect2:4 Identify Environmental Assumptions | 
|6  | Tue 20 Oct | Lab6   | 6    |        | Sect2:5/6 Develop Functional Architecture  |    
|7  | Tue 27 Oct |        |      |        | Sect2.7 Identify System Modes              | 
|8  | Tue 03 Nov | Lab7   | 7    |        | Sect2:8 Develop Performance Constraints    |             
|9  | Tue 10 Nov | Assign |      | Assign | Sect2:9 Define Software Requirements       |
|10 | Tue 17 Nov |        | 8    |        | Sect2:10 Allocate Subsystem Requirements   |
|11 | Tue 24 Nov | Lab8   |      |        | Sect2.11 Provide Rationale                  
|12 | Tue 01 Dec | Project| 9    | Project|                                            |
|13 | Tue 01 Dec | Project|      |        |                                            |
|   | Wed 09 Dec | Exam   | 9am  | ACE007 |                                            |             

===== 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 Quizzes.