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

Lecture notes are linked below, including lecture videos marked with (V) and supporting slides marked with (S). Slides do not always cover the full lecture. The lecture notes are significantly updated this semester, but the lecture videos are from Spring 2016.

Schedule

DateLecture NotesExtraDue
Tue 01/17Cyber-physical systems: introduction(V) (S
Thu 01/19Differential equations & domains(V) (S
Fri 01/20Rec: ODE, FOL, prepAsst 0 
Tue 01/24Choice & control(V) (S
Thu 01/26Safety & contracts(V) (SLab 0 
Fri 01/27Rec: Programs, properties, transitions, and examplescode 
Tue 01/31Dynamical systems & dynamic axioms(V) (Scode LICS'12
Thu 02/02Truth & proof(V) (SAsst 1 
Fri 02/03Rec: What is a proof and why?code Beta 1 
Tue 02/07Control loops & invariants(V) (Scode 
Thu 02/09Events & responses(V) (Scode Lab 1 
Fri 02/10Rec: Eventful tactical proofs in KeYmaera Xcode 
Tue 02/14Reactions & delays(V) (Scode 
Thu 02/16Differential equations & differential invariants(V) (Scode Asst 2 
Fri 02/17Rec: Events to delays and flying with differential invariantscode Beta 2 
Tue 02/21Differential equations & proofs(V) (Scode 
Thu 02/23Ghosts & differential ghosts(V) (Scode LMCS'12, extraLab 2 
Fri 02/24Rec: Differential invariants, differential cuts, rolling down a hillcode 
Tue 02/28Reviewing logical foundations & CPS(V) (SLICS'12Asst 3 
Thu 03/02Midterm
Fri 03/03Rec: Proving differential equations with cuts and differential ghostscode Beta 3 
Tue 03/07Differential invariants & proof theory(V) (SLMCS'12
Thu 03/09Verified models & verified runtime validation(V) (SFMSD'16Lab 3 
Fri 03/10Mid-semester break
Tue 03/14Spring break
Thu 03/16Spring break
Fri 03/17Spring break
Tue 03/21Hybrid systems & games(V) (STOCL'15
Thu 03/23Winning strategies & regions(V) (STOCL'15Asst 4 
Fri 03/24Rec: Game semantics, Geri's game, and Bus gamescode Beta 4 
Tue 03/28Winning & proving hybrid games(V) (Scode TOCL'15
Thu 03/30Game proofs & separations(V) (STOCL'15 TOCL'17Lab 4 
Fri 03/31Rec: Fun and games with proofscode White paper 
Tue 04/04Axioms & uniform substitutions(V) (SJAR'16
Thu 04/06Differential axioms & uniform substitutions(V) (SJAR'16Asst 5 
Fri 04/07Rec: Uniform subst and review
Tue 04/11Recap
Thu 04/13Final exam
Fri 04/14Rec: Project modeling, baseball proving, decomposing models, logical model-predictive controlcode 
Tue 04/18Optional: Safety & CPS ImplementationsProposal 
Thu 04/20Spring Carnival
Fri 04/21Spring Carnival
Tue 04/25Virtual substitution & real equations(V) (S
Thu 04/27Virtual substitution & real arithmetic(V) (S) , extra
Fri 04/28Rec: Real arithmetic for realcode 
Tue 05/02Distributed systems & hybrid systems(V) (SLMCS'12
Thu 05/04Hybrid systems & complete proofs(SLICS'12Project 
Fri 05/05Rec: Prepare for Grand PrixPaper 
Thu 05/11CPS V&V Grand PrixSlides 
The lecture schedule is tentative!

Lab Schedule

PointsAssignmentDue
Asst 00Preparation AssignmentFri 01/20
Lab 010Scavenger HuntcodeThu 01/26
Asst 160Introduction to Hybrid ProgramsThu 02/02
Beta 120Charging Station (Betabot)codeFri 02/03
Lab 170Charging Station (Veribot)codeThu 02/09
Asst 260Loops and ProofscodeThu 02/16
Beta 220Follow the Leader (Betabot)codeFri 02/17
Lab 280Follow the Leader (Veribot)codeThu 02/23
Asst 360Proofs, Diamonds, Differential InvariantsTue 02/28
Beta 320Robots on Racetracks (Betabot)codeFri 03/03
Lab 380Robots on Racetracks (Veribot)codeThu 03/09
Asst 460Differential Invariants, Cuts, and Being GhostlyThu 03/23
Beta 420Static and Dynamic Obstacles (Betabot)codeFri 03/24
Lab 480Static and Dynamic Obstacles (Veribot)codeThu 03/30
Asst 560Play Around with Hybrid GamesThu 04/06
White paper20Star-lab White PaperFri 03/31
Proposal80Star-lab ProposalTue 04/18
Project100Star-lab Final ProjectThu 05/04
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.