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.

Ablaufplan (vorläufig)

• 20. April: Vorbesprechung
• 27. April: Themenvergabe + Tips zur Literaturrecherche
• 4. Mai: Aspekte guter Präsentation
• 11. Mai: Lightning Talks
• 18. Mai: entfällt (Christi Himmelfahrt)
• 25. Mai: Hinweise zur Ausarbeitung

Präsentationen (je zwei pro Termin):

• 1. Juni
• 8. Juni: entfällt (Fronleichnam)
• 15. Juni
• 22. Juni
• 29. Juni
• 6. Juli
• 13. Juli
• Freitag 15. September: Abgabe der Ausarbeitung

Themenliste (vorläufig)

Model Checking und Algorithmen

• 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
• Der Simplex Algorithmus (eigene Literaturrecherche)
• Die Runge Kutta Methode (eigene Literaturrecherche)

Verifikation von Machinelearning

• Krasowski et al., Safe Reinforcement Learning for Urban Driving using Invariably Safe Braking Sets, 2022
• Tran et al., NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems, 2020

Analytische Methoden

• Prajna et al., Safety Verification of Hybrid Systems Using Barrier Certificates, 2004
• Quesel et al., How to model and prove hybrid systems with KeYmaera: a tutorial on safety, 2016

Real-time Temporallogik

• Gressenbuch et al., Predictive Monitoring of Traffic Rules, 2021
• Donzé et al., Robust Satisfaction of Temporal Logic over Real-Valued Signals, 2010

Verschiedenes

• Maierhofer et al., Formalization of Intersection Traffic Rules in Temporal Logic, 2022
• Wilhelm et al., The worst-case execution-time problem - overview of methods and survey of tools, 2008

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			Sa 01 Jul 2023 00:00 – Di 01 Aug 2023 00:00	Nicht zur Prüfung angemeldet

Termine

Art	Zeit	Regulärer Raum	Notiz
Wöchentliches Meeting	Do 10:15–12:00	Oettingenstr 67, U133