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

15-424 Foundations of Cyber-Physical Systems
15-624 Foundations of Cyber-Physical Systems
(Fall 2013)
Instructor: André Platzer
(office: Mon 4:20-5:30, GHC 9103)
Sarah Loos
(office: Tue 4:30-5:30 9th floor kitchenette
Fri 3:00-3:30, 4:20-5:00, GHC 4102)
Units: 12
Semester: Fall 2013
Time: MW 3-4:20
Place: GHC 4102
Recitation: F 3:30, GHC 4102
This course is listed in the Computer Science Department as 15-424/15-624 at Carnegie Mellon University. It counts as a Logics/Languages elective in the Computer Science curriculum.
Lec. Notes Piazza Course Staff KeYmaera Autolab
15-424: Foundations of Cyber-Physical Systems -- Schedule (Fall 2013)
Cyber-physical systems (CPSs) combine cyber capabilities (computation and/or communication) with physical capabilities (motion or other physical processes). Cars, aircraft, and robots are prime examples, because they move physically in space in a way that is determined by discrete computerized control algorithms. Designing these algorithms to control CPSs is challenging due to their tight coupling with physical behavior. At the same time, it is vital that these algorithms be correct, since we rely on CPSs for safety-critical tasks like keeping aircraft from colliding. In this course we will strive to answer the fundamental question posed by Jeannette Wing:
"How can we provide people with cyber-physical systems they can bet their lives on?"

Students who successfully complete this course will:

  • Understand the core principles behind CPSs.
  • Develop models and controls.
  • Identify safety specifications and critical properties of CPSs.
  • Understand abstraction and system architectures.
  • Learn how to design by invariant.
  • Reason rigorously about CPS models.
  • Verify CPS models of appropriate scale.
  • Understand the semantics of a CPS model.
  • Develop an intuition for operational effects.

The cornerstone of our course design are hybrid programs (HPs), which capture relevant dynamical aspects of CPSs in a simple programming language with a simple semantics. One important aspect of HPs is that they directly allow the programmer to refer to real-valued variables representing real quantities and specify their dynamics as part of the HP.

This course will give you the required skills to formally analyze the CPSs that are all around us -- from power plants to pace makers and everything in between -- so that when you contribute to the design of a CPS, you are able to understand important safety-critical aspects and feel confident designing and analyzing system models. It will provide an excellent foundation for students who seek industry positions and for students interested in pursuing research.

15-122 Principles of Imperative Computation (or equivalent)
15-251 Great Theoretical Ideas in Computer Science (or equivalent)
21-122 Integration, Differential Equations, and Approximation (or equivalent)
This course covers the basic required mathematical and logical background of cyber-physical systems. You will be expected to follow extra background reading material, which we will provide, as needed.
This course counts as a Logics/Languages elective in the Computer Science curriculum.
TEXTBOOK: (optional)
  1. André Platzer.
    Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics.
    Springer, 2010. 426 pages. ISBN 978-3-642-14508-7.
    [bib | doi | book | web | abstract]

  2. André Platzer.
    Foundations of Cyber-Physical Systems.
    Lecture Notes, Computer Science Department, Carnegie Mellon University. 2013.
    [bib | pdf | course | abstract]

  1. [e-book in CMU Library]
Logical Analysis of Hybrid Systems
Grading will be based on a set of homework assignments (20%), labs (50%), a midterm exam (10%), and a final exam (20%). Grading is based on points giving the above percentages approximately.
Midterm: 150 points, Wed 10/09 during lecture time. Closed book, one double-sided sheet of hand-written notes permitted.
Final: 300 points, 12/12 1pm-4pm, GHC 4307. Closed book, one double-sided sheet of hand-written notes permitted.

The instructors greatly appreciate the help by other members of the Logical Systems Lab, especially Khalil Ghorbal, Stefan Mitsch, Jan-David Quesel.