## Real-Time Systems and Temporal Verification

**Fall 2019**

**Instructor**: Stanley Bak

**Email:** Stanley.Bak@georgetown.edu

## Remaining Due Dates

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

## Useful Files

Course Project Tasks and Dates

Propositional / Predicate Logic Rules

## Homework

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

## Lectures and Supplemental Readings

**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

1**0/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)