Formale Methoden für Cyber-Physical Systems

Worum geht's

Du lernst formale Methoden zur Verifikation, Regelung, Beobachtung und Identifikation von Cyber‑Physical Systems (z. B. autonome Fahrzeuge, Roboter, Smart Grids). Am Ende kannst du Systeme mithilfe von Mengenrepräsentationen, Reachability‑Analyse und korrekt‑durch‑Konstruktions Methoden verifizieren und praktisch anwenden.

Was du danach kannst

• Vorteile formaler Methoden gegenüber nicht‑bewiesenen Methoden verstehen
• Intervallarithmetik und Abschätzungen mit Taylor‑Modellen anwenden
• Mengenrepräsentationen (Intervalle, Zonotope, Ellipsoide, Polytop, nicht‑konvexe Mengen) konstruieren
• Mengenrepräsentationen exakt oder über‑approximativ umwandeln
• Mengenoperationen (lineare Abbildungen, Minkowski‑Summe, konvexe Hülle) berechnen
• Software zur Propagation erreichbarer Mengen für lineare, nichtlineare und hybride Systeme implementieren
• Dynamische Systeme abstrakt beschreiben und Abstraktionsfehler berechnen
• Laufzeitverifikation in unsicheren/dynamischen Umgebungen umsetzen
• Reinforcement Learning mit formalen Methoden absichern
• Formell korrekte Regler automatisch synthetisieren unter Eingangs‑ und Zustandsbeschränkungen
• Reachability‑Analyse in Model Predictive Control integrieren für robuste/adaptive Regelung
• Mengbasierte Zustandsabschätzung mittels set‑based Observers durchführen
• Unterschiede zwischen Set‑Membership‑Ansatz und Interval‑Observer verstehen
• Prüfen, ob ein Modell alle realen Verhaltensweisen umfasst
• Modelle so mit Unsicherheit versehen, dass sie alle beobachteten Verhaltensweisen einschließen

Aus was das Modul besteht

• VorlesungVermittlung der theoretischen Grundlagen mittels Vortragsfolien und Tafelergänzungen
• Übung/ProgrammierungPraktische Programmieraufgaben zu den Vorlesungsinhalten, Vorbereitung auf Programmierprüfungen

Lehrmethode

• Vorlesung mit Folien und TafelErklären der Theorie und Ausarbeitung wichtiger Inhalte während der Lehrveranstaltung
• Programmierübungen zum SelbststudiumAnwenden der Methoden in Software; Lösungen werden präsentiert und diskutiert, Vorbereitung auf Prüfungen