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

• Sep 16 during class: Quiz 1 (based on Lab1) ✓
• Due date Project Phase 1a: Tuesday September 23, noon ✓
• Sep 23, during class: Quiz 2 (based on Lab2) ✓
• Sep 30, during class: Quiz 3 (based on Lab3) ✓
• Due date Project Phase 1b: MONDAY October 6, 4pm. Projects can be submitted up to noon on Tuesday October 7th.✓
• Oct 14, during class: Quiz 4 (based on Lab4 and Lab5)✓
• Thursday Nov 10 by noon: Assignment 1✓
• Tuesday Nov 11 during class: Quiz 5✓
• Thursday Nov 20 by noon: Assignment 2✓
• Thursday Nov 27 by noon: Project Phase2✓ (can be handed in until Monday Dec 1 without penalty)
• Exam: Thu, 11 Dec 2014 9:00 180 ACE 003 (Accolade Building East)

<hi cyan> Each Lab has some reading/preparation to do before the Lab.</hi>

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