course_outline
This is an old revision of the document!
Table of Contents
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
- 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
- Wednesday Nov 20 by noon: Assignment 2
- Thursday Nov 27 by noon: Project Phase2
TENTATIVE Schedule
<hi cyan> Each Lab has some reading/preparation to do before the Lab.</hi>
| Week | Date | PVS Exercise | Quiz | Assignment | Project |
|---|---|---|---|---|---|
| 1 | Tue 09 Sep | Lab 1 | |||
| 2 | Tue 16 Sep | Lab 2 | 1 | ||
| 3 | Tue 23 Sep | Lab 3 | 2 | Phase 1a due | |
| 4 | Tue 30 Sep | Lab 4 | 3 | ||
| 5 | Tue 07 Oct | Lab 5 | Phase 1b due (Mon) | ||
| 6 | Tue 14 Oct | 4 | |||
| 7 | Tue 21 Oct | Lab 6 | |||
| 8 | Tue 28 Oct | ||||
| 9 | Tue 04 Nov | Lab 7 | |||
| 10 | Tue 11 Nov | 5 | A1 due | ||
| 11 | Tue 18 Nov | A2 due | |||
| 12 | Tue 25 Nov | Phase 2 due | |||
| 13 | Tue 02 Dec | ||||
| Thu 11 Dec | Exam | ||||
Week 1
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
- PVS as a specification language. Mathematical thinking vs. Computational Thinking.
- 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.
course_outline.1415243154.txt.gz · Last modified: 2014/11/06 03:05 by jonathan