15-424: Foundations of Cyber-Physical Systems (Sp'17)

Lecture notes and S'16 lecture videos, marked with (V), as well as further reading material will be made available on this page as the semester progresses. The lecture notes are significantly updated this semester, but the lecture videos are from Spring 2016. The supporting slides, marked with (S), are made available too, but do not always cover the full lecture.

Schedule

DateLectureReadingDue
Tue 01/17Cyber-physical systems: introduction(V) (S
Thu 01/19Differential equations & domains
Fri 01/20Rec: ODE, FOL, prepAsst 0 
Tue 01/24Choice & control
Thu 01/26Safety & contracts Lab 0 
Fri 01/27Rec: Programs, properties, transitions, and examples
Tue 01/31Dynamical systems & dynamic axioms LICS'12
Thu 02/02Truth & proof Asst 1 
Fri 02/03Rec: What is a proof and why?Beta 1 
Tue 02/07Control loops & invariants
Thu 02/09Events & responsesLab 1 
Fri 02/10Rec: Eventful tactical proofs in KeYmaera X
Tue 02/14Reactions & delays
Thu 02/16Differential equations & differential invariants Asst 2 
Fri 02/17Rec: Events to delays and differential invariantsBeta 2 
Tue 02/21Differential equations & proofs
Thu 02/23Ghosts & differential ghosts LMCS'12 Lab 2 
Fri 02/24Rec: Differential invariants, differential cuts, differential ghosts
Tue 02/28Reviewing logical foundations & CPS LICS'12 Asst 3 
Thu 03/02Midterm
Fri 03/03Rec: Debugging models, understanding failed proofs, differential cutsBeta 3 
Tue 03/07Differential invariants & proof theory LMCS'12
Thu 03/09Verified models & verified runtime validation FMSD'16 Lab 3 
Fri 03/10Mid-semester break
Tue 03/14Spring break
Thu 03/16Spring break
Fri 03/17Spring break
Tue 03/21Hybrid systems & games TOCL'15
Thu 03/23Winning strategies & regions TOCL'15
Fri 03/24Rec: Game examples with fun and subtletyBeta 4 
Tue 03/28Winning & proving hybrid games TOCL'15 Asst 4 
Thu 03/30Game proofs & separations TOCL'15
Fri 03/31Rec: Fun and proofs with gamesLab 4 
Tue 04/04Axioms & uniform substitutions JAR'16 White paper 
Thu 04/06Differential axioms & uniform substitutions JAR'16
Fri 04/07Rec: Logical model-predictive control
Tue 04/11RecapAsst 5 
Thu 04/13Final exam
Fri 04/14Rec: Final posteriorProposal 
Tue 04/18TBD
Thu 04/20Spring Carnival
Fri 04/21Spring Carnival
Tue 04/25Virtual substitution & real equations
Thu 04/27Virtual substitution & real arithmetic
Fri 04/28Rec: Real arithmetic for real
Tue 05/02Distributed systems & hybrid systems LMCS'12
Thu 05/04Model checking & reachability analysis
Fri 05/05Rec: Prepare for Grand PrixProject Paper 
Thu 05/11CPS V&V Grand PrixSlides 
The lecture schedule is tentative!
Reading: Provides optional additional reading material in addition to the lecture notes, which are the primary source.

Lab Schedule

PointsAssignmentDue
Asst 00Preparation AssignmentFri 01/20
Lab 010Scavenger HuntThu 01/26
Asst 160Introduction to Hybrid ProgramsThu 02/02
Beta 120Charging Station (Betabot)Fri 02/03
Lab 170Charging Station (Veribot)Thu 02/09
Asst 260Loops and ProofsThu 02/16
Beta 220Follow the Leader (Betabot)Fri 02/17
Lab 280Follow the Leader (Veribot)Thu 02/23
Asst 360Proofs, Diamonds, Differential InvariantsTue 02/28
Beta 320Robots on Racetracks (Betabot)Fri 03/03
Lab 380Robots on Racetracks (Veribot)Thu 03/09
Asst 460Differential Invariants and Cut-in DifferentiallyTue 03/28
Beta 420Static and Dynamic Obstacles (Betabot)Fri 03/24
Lab 480Static and Dynamic Obstacles (Veribot)Fri 03/31
Asst 560Play Around with Hybrid GamesTue 04/11
White paper20Star-lab White PaperTue 04/04
Proposal80Star-lab ProposalFri 04/14
Project100Star-lab Final ProjectFri 05/05
Paper100Term PaperFri 05/05
Slides0Slides and PresentationThu 05/11
Sum1000points listed

The Lab and Assignment Schedule is tentative!
Labs have a due date and time for Betabots (due at start of lecture/recitation) and a different due date and time for Veribots (due at midnight). Theory assignments are due by midnight on the due day.

For an overview of the labs, see Labs & Assignments.