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

Schedule

Date		Lecture Notes	Extra	Due
Mon	08/25	Cyber-physical systems: introduction	Ch 1
Wed	08/27	Differential equations & domains	Ch 2.2,2.3,App.B
Fri	08/29	Rec: ODE, FOL, prep		Asst 0
Mon	09/01	Free: Labor Day (no class)
Wed	09/03	Choice & control	Ch 2.2,2.3	Lab 0
Fri	09/05	Rec: HP: Syntax, semantics, example
Mon	09/08	Safety & contracts	Ch 2.2,2.3
Wed	09/10	Dynamical systems & dynamic axioms	Ch 2.5.2	Asst 1 Beta 1
Fri	09/12	Rec: Did you prove what you meant to prove?
Mon	09/15	Truth & proof	Ch 2.5.2,App.A
Wed	09/17	Control loops & invariants	code Ch 2.5.2&4	Lab 1
Fri	09/19	Rec: Manual proofs and KeYmaera proofs	code
Mon	09/22	Events & responses	code
Wed	09/24	Reactions & delays	code	Asst 2 Beta 2
Fri	09/26	Rec: Events to delays	code
Mon	09/29	Differential equations & differential invariants	code Ch 3.5
Wed	10/01	Differential equations & proofs	code Ch 3.5	Lab 2
Fri	10/03	Rec: Differential invariants, differential cuts	code
Mon	10/06	Recap		Asst 3
Wed	10/08	Midterm
Fri	10/10	Rec: Stuff
Mon	10/13	Ghosts & differential ghosts	code LMCS'12
Wed	10/15	Differential invariants & proof theory	LMCS'12	Beta 3
Fri	10/17	Free: Mid-semester break
Mon	10/20	Logical foundations & CPS	code LICS'12
Wed	10/22	Differential & temporal logic	Ch 4	Lab 3
Fri	10/24	Rec: Proof intuitions, KeYmaera specifics	code	Asst 4
Mon	10/27	Differential & temporal proofs	code Ch 4
Wed	10/29	Virtual substitution & real equations	App.D	Beta 4
Fri	10/30	Rec: dTL semantics
Mon	11/03	Virtual substitution & real arithmetic	App.D
Wed	11/05	Verified models & verified CPS runtime validation	RV'14	Lab 4
Fri	11/07	Rec: Safety in motion, real arithmetic		Asst 5 White paper
Mon	11/10	Hybrid systems & games	pdf
Wed	11/12	Winning strategies & regions	pdf
Fri	11/14	Rec: Game examples
Mon	11/17	Winning & proving hybrid games	pdf	Proposal
Wed	11/19	Game proofs & separations	code ,pdf
Fri	11/21	Rec: Game proofs
Mon	11/24	Free: Project Day (no class)
Wed	11/26	Free: Thanksgiving (no class)
Fri	11/28	Free: Thanksgiving (no class)
Mon	12/01	Logical theory & completeness
Wed	12/03	Final exam
Fri	12/05	Rec: Wrap-up, recap
Sun	12/07	Free: Weekend (no class)		Project
Mon	12/08	Free: Finals week (no class)
Tue	12/09	Free: Finals week (no class)		Paper
Wed	12/10	CPS V&V Grand Prix		Presentation

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

	Points	Assignment		Due
Asst 0	0	Preparation Assignment		Fri	08/29
Lab 0	10	Scavenger Hunt	code	Wed	09/03
Asst 1	60	Introduction to Hybrid Programs		Wed	09/10
Beta 1	20	Charging Station (Betabot)	code	Wed	09/10
Lab 1	70	Charging Station (Veribot)	code	Wed	09/17
Asst 2	60	Loops and Proofs		Wed	09/24
Beta 2	20	Follow the Leader (Betabot)	code	Wed	09/24
Lab 2	80	Follow the Leader (Veribot)	code	Wed	10/01
Asst 3	60	Proofs, Diamonds, Differential Invariants		Mon	10/06
Beta 3	20	Robots on Racetracks (Betabot)	code	Wed	10/15
Lab 3	80	Robots on Racetracks (Veribot)	code	Wed	10/22
Asst 4	60	Differential Invariants and Nondeterministic Assignment		Fri	10/24
Beta 4	20	Static and Dynamic Obstacles (Betabot)	code	Wed	10/29
Lab 4	80	Static and Dynamic Obstacles (Veribot)	code	Wed	11/05
Asst 5	60	Differential Auxiliaries, dTL, Quantifier Elimination		Fri	11/07
White paper	20	Star-lab White Paper		Fri	11/07
Proposal	80	Star-lab Proposal		Mon	11/17
Project	100	Star-lab Final Project		Sun	12/07
Paper	100	Term Paper		Tue	12/09
Presentation	0	Slides and Presentation		Wed	12/10
Sum	1000	points 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.