Formale Methoden für Cyber-Physical Systems

• Prüfungen
  • Seminarnote

Beschreibung

Inhalte

Eingebettete Systeme oder auch Cyber-Physical Systems (CPS) sind diejenigen
Systeme bei denen Software und Hardware korrekt zusammen arbeiten.
Die in der Softwareentwicklung angewandten Methoden wie Testen, statische
Analyse und Formale Spezifikation und Verifikation lassen sich auch auf
diese Systemklasse übertragen. Voraussetzung ist allerdings, dass ein Modell
des physikalischen Systemverhaltens vorliegt, das z.B. simuliert werden kann.
Solche physikalischen Modelle werden typischerweise mit Differenzialgleichungen
als sogenannte “hybride Systeme” beschrieben.

In diesem Seminar stellen die SeminarteilnehmerInnen jeweils einen Ansatz
oder ein wissenschaftliches Papier vor und experimentieren mit den
jeweiligen dazugehörigen Tools.

Anforderungen

• selbstständige Literaturrecherche
• eigensständige praktische Experimente mit den Tools
• mündliche Präsentation (ca 20 min)
• schriftliche Ausarbeitung (ca 8-10 Seiten im LNCS Format)

Empfohlene Vorkenntnisse:
- Formale Spezifikation und Verifikation
- Logik und Diskrete Strukturen

Hinweis: Sie sind selbst verantwortlich für das Einhalten guter
wissenschaftlicher Praxis, dazu gehört korrektes Zitieren in allen Dokumenten
(Präsentation, Text, auch im Entwurf!), Verstöße führen direkt zum
nicht-Bestehen des Seminars. Wir besprechen die Regeln eingangs ganz konkret.
Mit eigenen Worten und einer eigenen Struktur werden Sie diese Regeln leicht
einhalten können.

Themenliste (vorläufig)

Das folgende Buch kann zusätzlich von Interesse sein bei Themen, die mit LFCPS markiert sind:

• Platzer, Logical Foundations of Cyber-Phyiscal Systems (LFCPS), 2018

Algorithmische Analyse

• Alur et al., Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems, 1993
• Alur et al., The Theory of Timed Automata, 1991
• Tarski, A Decision Method for Elementary Algebra and Geometry, 1951 + LFCPS

Logiken für hybride Systeme

• Platzer, Differential Dynamic Logic for Hybrid Systems, 2008 + LFCPS
• Plazter, Differential Game Logic, 2015 + LFCPS
• Platzer, A Differential Operator Approach to Equational Differential Invariants - (Invited Paper), 2012 + LFCPS

Modellierung

• Krasowksi et al., Temporal Logic Formalization of Marine Traffic Rules, 2021
• Shalev et al., On a Formal Model of Safe and Scalable Self-driving Cars, 2017

Analytische Methoden

• Prajna et al., Safety Verification of Hybrid Systems Using Barrier Certificates, 2004
• Jagtap et al., Compositional construction of control barrier functions for interconnected control systems, 2020

Testen

• Ernst et al., Falsification of Hybrid Systems Using Adaptive Probabilistic Search, 2021
• Annpureddy et al., S-TaLiRo: A Tool for Temporal Logic Falsification for Hybrid Systems, 2011
• Donzé, Breach, A Toolbox for Verification and Parameter Synthesis of Hybrid Systems, 2010
• Akazaki et al., Falsification of Cyber-Physical Systems Using Deep Reinforcement Learning, 2018
• Menghi et al., Approximation-refinement testing of compute-intensive cyber-physical models: an approach based on system identification, 2020
• Waga, Falsification of cyber-physical systems with robustness-guided black-box checking, 2020
• Zhang et. al., Effective Hybrid System Falsification Using Monte Carlo Tree Search Guided by QB-Robustness, 2021

Echtzeitprogrammierung

• Liu et al., Scheduling Algorithms for Multiprogramming in a Hard-Real-Time Environment, 1973

Ablaufplan (vorläufig)

• 18. Oktober: Vorbesprechung
• 25. Oktober: Themenvergabe + Tips zur Literaturrecherche
• 1. November: entfällt (Allerheiligen)
• 8. November: Lightning Talks
• 15. November: Aspekte guter Präsentation
• 22. November: Hinweise zur Ausarbeitung

Präsentationen (je zwei pro Termin):

• 29. November
• 6. November
• 13. November
• 20. November
• 10. Januar
• 17. Januar

Institut

Institut für Informatik

Dozent:in

• Gidon Ernst

Assistent:in

• Marvin Brieger

Kursteilnehmer:innen

10 von 12

Zentralanmeldung

Bachelorseminare

Anweisungen zur Anmeldung

Bitte keine zusätzlichen Bewerbungen einreichen, wir nehmen keinen Einfluss auf die Verteilung der Seminarplätze.

Material

Das Kursmaterial ist nur für Mitglieder des Kurses einsehbar, also z.B. für Teilnehmer:innen, Tutor:innen, Korrektor:innen und Verwalter:innen.

Prüfungen

Name	Anmeldung ab	Anmeldung bis	Termin	Prüfungsanmeldung
Seminarnote				Nicht zur Prüfung angemeldet

Termine

Art	Zeit	Regulärer Raum	Notiz
Wöchentliches Meeting	Di 10:15–12:00	Oettingenstraße 67, U133