15-424: Foundations of Cyber-Physical Systems (Fa'14)

Schedule

DateLectureReadingDue
Mon 08/25Cyber-physical systems: introductionCh 1
Wed 08/27Differential equations & domainsCh 2.2,2.3,App.B
Fri 08/29Rec: ODE, FOL, prepAsst 0 
Mon 09/01Labor Day (no class)
Wed 09/03Choice & controlCh 2.2,2.3Lab 0 
Fri 09/05Rec: HP: Syntax, semantics, example
Mon 09/08Safety & contractsCh 2.2,2.3
Wed 09/10Dynamical systems & dynamic axiomsCh 2.5.2Asst 1 Beta 1 
Fri 09/12Rec: Did you prove what you meant to prove?
Mon 09/15Truth & proofCh 2.5.2,App.A
Wed 09/17Control loops & invariantscode Ch 2.5.2&4Lab 1 
Fri 09/19Rec: Manual proofs and KeYmaera proofscode 
Mon 09/22Events & responsescode 
Wed 09/24Reactions & delayscode Asst 2 Beta 2 
Fri 09/26Rec: Events to delayscode 
Mon 09/29Differential equations & differential invariantscode Ch 3.5
Wed 10/01Differential equations & proofscode Ch 3.5Lab 2 
Fri 10/03Rec: Differential invariants, differential cutscode 
Mon 10/06RecapAsst 3 
Wed 10/08Midterm
Fri 10/10Rec: Stuff
Mon 10/13Ghosts & differential ghostscode LMCS'12
Wed 10/15Differential invariants & proof theoryLMCS'12Beta 3 
Fri 10/17Mid-semester break
Mon 10/20Logical foundations & CPScode LICS'12
Wed 10/22Differential & temporal logicCh 4Lab 3 
Fri 10/24Rec: Proof intuitions, KeYmaera specificscode Asst 4 
Mon 10/27Differential & temporal proofscode Ch 4
Wed 10/29Virtual substitution & real equationsApp.DBeta 4 
Fri 10/30Rec: dTL semantics
Mon 11/03Virtual substitution & real arithmeticApp.D
Wed 11/05Verified models & verified CPS runtime validationRV'14Lab 4 
Fri 11/07Rec: Safety in motion, real arithmeticAsst 5 White paper 
Mon 11/10Hybrid systems & gamespdf
Wed 11/12Winning strategies & regionspdf
Fri 11/14Rec: Game examples
Mon 11/17Winning & proving hybrid gamespdfProposal 
Wed 11/19Game proofs & separationscode ,pdf
Fri 11/21Rec: Game proofs
Mon 11/24Project Day (no class)
Wed 11/26Thanksgiving (no class)
Fri 11/28Thanksgiving (no class)
Mon 12/01Logical theory & completeness
Wed 12/03Final exam
Fri 12/05Rec: Wrap-up, recap
Sun 12/07Weekend (no class)Project 
Mon 12/08Finals week (no class)
Tue 12/09Finals week (no class)Paper 
Wed 12/10CPS V&V Grand PrixPresentation 
The lecture schedule is tentative!
Reading: The chapters Ch i.j for further reading refer to chapters in the textbook in addition to the lecture notes.

Lab Schedule

PointsAssignmentDue
Asst 00Preparation AssignmentFri 08/29
Lab 010Scavenger HuntcodeWed 09/03
Asst 160Introduction to Hybrid ProgramsWed 09/10
Beta 120Charging Station (Betabot)codeWed 09/10
Lab 170Charging Station (Veribot)codeWed 09/17
Asst 260Loops and ProofsWed 09/24
Beta 220Follow the Leader (Betabot)codeWed 09/24
Lab 280Follow the Leader (Veribot)codeWed 10/01
Asst 360Proofs, Diamonds, Differential InvariantsMon 10/06
Beta 320Robots on Racetracks (Betabot)codeWed 10/15
Lab 380Robots on Racetracks (Veribot)codeWed 10/22
Asst 460Differential Invariants and Nondeterministic AssignmentFri 10/24
Beta 420Static and Dynamic Obstacles (Betabot)codeWed 10/29
Lab 480Static and Dynamic Obstacles (Veribot)codeWed 11/05
Asst 560Differential Auxiliaries, dTL, Quantifier EliminationFri 11/07
White paper20Star-lab White PaperFri 11/07
Proposal80Star-lab ProposalMon 11/17
Project100Star-lab Final ProjectSun 12/07
Paper100Term PaperTue 12/09
Presentation0Slides and PresentationWed 12/10
Sum1000points listed

The Lab and Assignment Schedule is tentative!
Theory assignments are due at start of lecture on the due day.
Programming lab assignments are due at 22:00 on the due day.
Labs have a due date for Betabots and a due date for Veribots.

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