|
Schedule | ||||||||||||
|
|
- DESCRIPTION:
-
Hybrid systems analysis studies the question "how can we build computerized controllers for physical systems that are guaranteed to meet their design goals?" Application areas include safety-critical systems like adaptive cruise control technology for cars or auto pilots for aircraft collision avoidance. This course covers symbolic analysis techniques for safety-critical hybrid systems design. It will emphasize concise representations of analytic problems in logic and their algorithmic solutions in automated theorem provers and model checkers. It will also indicate elegant connections between the theory, practice and applications of hybrid systems analysis.
 |
 |
-
Of more general interest, the course provides a thorough introduction to logic and automated theorem proving techniques with their extensions to the logic-based analysis of hybrid systems. Starting from basic propositional logic, the class will develop the background in automatic proving and system analysis, including ground and free variable tableau procedures for first-order logic. It will cover extensions to dedicated verification logics for hybrid systems and their verification procedures.
The class will provide you with modern techniques for analyzing the correct functioning of important safety-critical systems ranging from embedded systems in cars and biomedical devices, over chemical/physical process control and chip design, to full car, aircraft, and train control. The opportunity to gain practical experience in analysis of cyber-physical systems will be given as part of the course. The class should be appropriate for graduate students in all areas and for advanced undergraduates with an interest in mathematical, logical, or formal analysis methods.
- OBJECTIVES:
- You will develop an understanding for important safety-critical aspects of embedded and cyber-physical systems. You will learn to understand and develop hybrid system models. You will learn how you can analyze if a hybrid system works correctly and if it actually meets its design goals. In addition, the course will provide you with a background and understanding in building and using automated theorem provers and verification algorithms. You will be able to use formal verification calculi to analyze system correctness and you will understand how automatic verification techniques work.
- PREREQUISITES:
- Basic knowledge in logic (e.g., propositional logic) and calculus (differential equations) is of advantage but not required.
- TEXT:
- Basic notes and background material will be handed out.
- METHOD OF EVALUATION:
-
Grading will be based on a set of homework assignments, including hands-on analysis experience, midterm exam, and a final project (30% Homework, 15% Midterm, 55% Project).
The project component will be one or several projects related to hybrid systems. - MORE INFORMATION:
- See case studies for some illustrations and examples of hybrid system applications.
- TOPICS TO BE COVERED:
-
- Safety-critical Hybrid Systems
- Numerical Analysis versus Symbolic Verification
- Propositional Logic
- Propositional Tableau Procedures
- First-order Logic
- First-order Tableau Procedures
- Dynamic Logic Programs and Dynamical Systems
- Hybrid Dynamical Systems & Hybrid Programs
- Aircraft, Train, and Car Control
- Dynamic Verification Calculi
- Decision Procedures
- Theorem Proving Modulo
- Differential Equations, Differential Variance and Invariance
- Disturbances in Hybrid Systems Control
- Time permitting: Proof Theory of Hybrid Systems
- Time permitting: Fixedpoint Model Checking Engines
- Time permitting: Automatic Verification