|
Questions Schedule Textbook Videos Diderot KeYmaera X Grand Prix |
||||||||||||||||
|
- NEWS:
-
- This course will use Diderot for quizzes, Q&A and assignments. If you do not have access to Diderot, look through your email for instructions on how to activate your account and drop me an email if it does not work.
- DESCRIPTION:
-
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 and their differential equations.
- Verify CPS models of appropriate scale.
- Understand the semantics of a CPS model.
- Develop an intuition for operational effects.
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.
- PREREQUISITES:
-
- 15-122 Principles of Imperative Computation (or equivalent)
- 21-120 Differential and Integral Calculus (or equivalent)
The 15-424 course counts as a Logics/Languages elective in the Computer Science curriculum. The 15-824 course fulfills the Programming Languages star requirement. - TEXTBOOK:
-
- METHOD OF EVALUATION:
-
Grading will be based on a set of homework assignments (11%), labs (27%), final project entering the CPS V&V Grand Prix worth 20%, midterm exams I+II (20%), and a function of your best quizzes (20%).
Grading is based on points giving the above percentages approximately.
The exact distribution of points is still in flux but will work roughly as indicated.
Midterm I: 150 points, Thu 10/15 during lecture time. Closed book, one double-sided sheet of hand-written notes permitted. Midterm II: 150 points, Thu 11/12, during lecture time. Closed book, one double-sided sheet of hand-written notes permitted. Grand Prix: Fri 12/18 during finals week, CPS V&V Grand Prix for presenting final projects to a panel of experts in CPS. - PRIOR INSTANCES:
- Prior instances of the course: F2013, F2014, S2016, S2017, F2018, F2019
The instructors greatly appreciate the help by other members of the Logical Systems Lab, especially Stefan Mitsch, on advancing KeYmaera X.