Differences

This shows you the differences between two versions of the page.

--- course_outline [2014/11/06 03:05] – jonathan
+++ course_outline [2014/12/15 02:59] (current) – jonathan
@@ Line 13: / Line 13: @@
   * 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
+  * Thursday Nov 10 by **noon**: Assignment 1✓
-  * Tuesday Nov 11 during class: Quiz 5
+  * Tuesday Nov 11 during class: Quiz 5✓
-  * Wednesday Nov 20 by **noon**: Assignment 2
+  * Thursday Nov 20 by **noon**: Assignment 2✓
-  * Thursday Nov 27 by **noon**: Project Phase2
+  * 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)
 ===== TENTATIVE Schedule =====
@@ Line 38: / Line 39: @@
 |   | Thu 11 Dec |            Exam               ||
-===== Week 1 =====
+===== Topics Covered =====
-**Required Readings and self-paced work**:
-  * Labs: PVS Lab0 and Lab1
-  * Text: REMH Chapter 1 (overview) and Chapter 2.1 (Develop System Overview).
-  * Note: It is assumed that you study the case studies (Appendix A, B, C and D) together with the text.
-SVN Notes1
+  *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.
-  * PVS as a specification language. Mathematical thinking vs. Computational Thinking.
+**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.
-  * PVS basic types and functions
-  * PVS propositional logic (the topic of Lab 1)
-SVN Notes2 (on a simple bank ATM, in preparation for Project Phase1)
-  * The System Under description as a black box
-  * The system boundary
-  * Monitored variables and events
-  * Controlled variables
-  * The input grammar (of monitored events or commands)
-  * The abstract state
-  * Use Cases (acceptance tests)
-  * Function tables
-Notes 3
-  * Using PVS to specify a digital circuit
-  * Simple Function Tables and completeness and disjointness
-  * Implementations, Specifications and proving that implementations satisfy specifications
-===== Week 2 =====
-**Required Readings and self-paced work**:
-  * Labs: PVS Lab2
-  * Text: REMH Chapter 2.2 (Identify System Boundary).
-  * Note: It is assumed that you study the case studies (Appendix A, B, C and D) together with the text.