0000002856 20W 4SWS VI Formal Methods for Cyber-Physical Systems   Hilfe Logo

LV - Detailansicht

Wichtigste Meldungen anzeigenMeldungsfenster schließen
Allgemeine Angaben
Formal Methods for Cyber-Physical Systems 
lecture with integrated exercises
Winter semester 2020/21
... alle LV-Personen
Informatics 6 - Chair of Robotics, Artificial Intelligence and Real-time Systems (Prof. Knoll)
(Contact information)
Allocations: 1 
Angaben zur Abhaltung
In many modern systems, computing elements are tightly connected with physical entities for which the term "cyber-physical systems" has been established in recent years. Examples are automated vehicles, surgical robots, smart grids, and collaborative human-robot manufacturing.

Because cyber-physical systems are becoming increasingly safety-critical due to the ongoing trend towards deeper autonomy, formal methods that prove the correct behavior of systems are gaining importance. This lecture teaches state-of-the-art formal methods by combining theory and hands-on programming sessions.

• Preliminaries: Set representations and operations, including interval arithmetic and Taylor models
• Formal verification using reachability analysis; considered system classes: linear systems, nonlinear systems, hybrid systems
• Online verification in uncertain and dynamic environments
• Safe reinforcement learning
• Correct-by-construction controller design
• Robust model predictive control
• Set-based observers: set-membership approach and interval-observer approach
• Conformance checking for system identification: observer-based approaches and reachability-based approaches
Cyber-Physical Systems (IN2305)
After attending the module, you are able to verify, control, observe, and identify cyber-physical systems in a provably correct way by using formal methods. The material is taught at a level that enables you to apply the methods for real problems or start a research project on formal methods for cyber-physical systems. In particular, you will acquire the following skills:

• You understand the benefits of formal methods compared to conventional methods which do not prove properties.
• You can apply interval arithmetic and bound evaluations of functions using Taylor models.
• You can construct set representations for intervals, zonotopes, ellipsoids, polytopes, and non-convex sets.
• You can convert set-representations exactly or in an over-approximative way.
• You can compute set-based operations, such as linear maps, Minkowski sum, or convex hull.
• You can write software to propagate reachable sets of linear, nonlinear, and hybrid systems.
• You can abstract dynamical systems to simpler descriptions and compute the associated abstraction error.
• You can create solutions to verify cyber-physical systems during runtime.
• You can safeguard reinforcement learning techniques using formal methods.
• You can automatically synthesize formally-correct controllers adhering to input and state constraints.
• You can integrate reachability analysis in model predictive control to design robust and adaptive controllers.
• You can estimate the set of possible states using set-based observers.
• You understand the difference between the set-membership approach and the interval-observer approach for set-based observers.
• You can check whether a model encloses all real behaviors.
• You can program solutions to add uncertainty to models so that they include all observed behaviors.

The module consists of a lecture and accompanying excercices. The content of the lecture is presented via slides, which are completed during the lecture using the blackboard.

In the accompanying excercices, students should solve programming tasks directly related to the taught content. These tasks should be solved at home. Possible solutions are presented during the excercices and compared with the developed solutions of the students. The programming exercises and the discussion during the excercice sessions prepare the students for the programming tests.
Für die Anmeldung zur Teilnahme müssen Sie sich in TUMonline als Studierende*r identifizieren.
There is not yet a suitable textbook available; we will provide research papers to deepen the understanding.
Online information
e-learning course (moodle)