Real-Time Systems and Temporal Verification
Fall 2019
Fall 2019
Instructor: Stanley Bak
Email: Stanley.Bak@georgetown.edu
Oct 22 (at start of class) - HW 2
Oct 31 (end of day, 11:59pm) - Project Literature Review
Nov 5 (at start of class) - Research Paper presentation #1 - Matt
Nov 12 (at start of class) - Research Paper presentation #2 - Caleb
Nov 19 (at start of class) - Research Paper presentation #3 - Rahel
Nov 26 (end of day, 11:59pm) - Project Report Draft
Dec 3 - Project Presentation #1 - Rahel
Dec 3 - Project Presentation #2 - Caleb
Dec 5 - Project Presentation #3 - Matt
Dec 9 (end of day, 11:59pm) - Final Project Report
Course Project Tasks and Dates
Propositional / Predicate Logic Rules
Homework 1 (Modified 9/16/2019. Due 9/24/2019 at the start of class. Code can be e-mailed to me.)
Homework 2 (Due 10/22/2019 at the start of class. Code should be e-mailed to me).
8/29/2019 Lecture 1 - Overview
Supplemental reading: https://www.seattletimes.com/business/boeing-aerospace/failed-certification-faa-missed-safety-issues-in-the-737-max-system-implicated-in-the-lion-air-crash/
9/3/2019 Lecture 2 - Propositional Logic
Supplemental reading: http://www-users.math.umn.edu/~arnold/disasters/ariane5rep.html
9/5/2019 Lecture 3 - Predicate Logic
Supplemental reading: https://cacm.acm.org/magazines/2017/8/219606-the-science-of-brute-force/fulltext
9/10/2019 Lecture 4 - Predicate Logic / SAT Tool Demo
9/12/2019 Lecture 5 - Hoare Logic
Supplemental reading: https://www.cs.cmu.edu/~crary/819-f09/Hoare69.pdf
9/17/2019 Lecture 6 - Hoare Logic, Part 2
9/19/2019 Lecture 7 - Abstract Interpretation
9/24/2019 Lecture 8 - Abstract Interpretation 2
HW1 Due!
9/26/2019 Lecture 9 - Predicate Abstraction and Lecture 9 - SAT
Supplemental Reading: Chaff: Engineering an Efficient SAT Solver
10/1/2019 Lecture 10 - SMT Solving
10/3/2019 Lecture 11 - Temporal Logic and Lecture 11 - Nelson Oppen
10/8/2019 Lecture 12 - Temporal Logic 2 and Model Checking Intro and Linear Temporal Logic
HW2 assigned
10/10/2019 Lecture 13 - Model Checking History and Computational Tree Logic
10/15/2019 Lecture 14 - CTL Examples - Computational Tree Logic
10/17/2019 Lecture 15 - Model Checking - Computational Tree Logic - LTL Model Checking
10/22/2019 Lecture 16 - LTL Model Checking
HW2 Due!
10/22/2019 Lecture 17 - Binary Decision Diagrams (BDDs) - BDD Operations
10/29/2019 Lecture 18 BDD and SAT Model Checking - BDD Operations
10/31/2019 Lecture 19 - Hybrid Automata - Timed Automata
11/5/2019 Lecture 20 - Reachability Analysis of Hybrid Automata
11/7/2019 Lecture 21 - Flowpipe Construction for Linear Systems - Logistics & HW
11/12/2019 Lecture 22 - Real-Time Systems Overview
HW Bonus Opportunity: Attend talk on Thursday, ask a question and hand in a 1-page summary for 25% bonus on last homework
11/14/2019 Lecture 23 - Real-Time Schedulability
Supplemental Reading: Liu, C. L., and Layland, J. W. "Scheduling algorithms for multiprogramming in a hard-real-time environment". Journal of the Association for Computing Machinery, 1973
11/19/2019 - Lecture 24 - Response Time Analysis
11/21/2019 - Special Lecture 25: Scalable Set-based Analysis for Verification of Cyber-Physical Systems (in Room 326, St. Mary's Hall)
11/26/2019 - Lecture 26: Scheduling Anomalies -Priority Inheritance Protocol (PIP) - Priority Ceiling Protocol (PCP)
12/3/2019 - Project Presentations (Rahel & Caleb)
12/5/2019 - Project Presentation (Matt)