Formale Methoden für Cyber-Physical Systems

What it is about

You will learn formal methods for verification, control, observation and identification of cyber-physical systems (e.g., autonomous vehicles, robots, smart grids). In the end you can verify and practically apply systems using set representations, reachability analysis and correct-by-construction methods.

What you will be able to do

• Understand advantages of formal methods over non-provable methods
• Apply interval arithmetic and Taylor model estimations
• Construct set representations (intervals, zonotopes, ellipsoids, polytopes, non-convex sets)
• Convert set representations exactly or over-approximately
• Compute set operations (linear mappings, Minkowski sum, convex hull)
• Implement software for propagation of reachable sets for linear, nonlinear and hybrid systems
• Abstractly describe dynamic systems and compute abstraction errors
• Implement runtime verification in unsafe/dynamic environments
• Secure reinforcement learning with formal methods
• Automatically synthesize formally correct controllers under input and state constraints
• Integrate reachability analysis in model predictive control for robust/adaptive control
• Perform set-based state estimation using set-based observers
• Understand the differences between set-membership approach and interval observer
• Check whether a model encompasses all real-world behaviors
• Characterize models with uncertainty so that they include all observed behaviors

What the module consists of

• VorlesungDelivery of the theoretical foundations via slides and board work
• Übung/ProgrammierungPractical programming tasks related to lecture content, preparation for programming exams

Teaching method

• Vorlesung mit Folien und TafelExplain the theory and work out important content during the course
• Programmierübungen zum SelbststudiumApply the methods in software; solutions are presented and discussed, preparation for exams