| Erweiterung von Simulink für Stochastische Modellierung: Integration und Übersetzung von stochastischen Blöcken |
Bachelor / Master |
Simulink ist eine Datenfluss-orientierte Modellierungssprache zum Entwurf und der Simulation von hybriden Systemen. Zur Analyse dieser Systeme wird aktuell eine Transformation von Simulink Modellen zu Hybriden Automaten entwickelt. Langfristig soll diese auch stochastische Komponenten abdecken. Im Rahmen einer Bachelor- oder Masterarbeit soll nun analysiert werden inwiefern bereits in den Simulink Modellen stochastische Komponenten integriert werden können und welche Arten von stochastischem Verhalten durch eigene Subsysteme umgesetzt werden können. Im Rahmen einer Masterarbeit könnte zusätzlich eine Übersetzung der stochastischen Simulink-Blöcke zu stochastischen hybriden Automaten entworfen werden. |
| Verbesserte Reinforcement Learning Bewertungen mittels Metriken in Hybriden Petri Netzen |
Bachelor |
In hybriden Petri Netzen können Entscheidungen mithilfe von Reinforcement Learning optimiert werden. Bisher werden diese basierend auf der Erfüllung einer Eigenschaft am Ende eines Simulationslaufes bewertet. Dies hat den großen Nachteil, dass sehr viel Training notwendig ist, um gute Entscheidungen zu lernen. Daa Ziel der Arbeit ist es, Metriken zu finden, mit welchen man schon während eines Simulationslauf sinnvolle Bewertungen geben kann. |
| Detektion und Eliminierung unsicherer Entscheidungen in Symbolischen Zustandsräumen |
Bachelor / Master |
Maschinelles Lernen wird in immer mehr sicherheitskritischen Bereichen erfolgreich eingesetzt, allerdings können schlechte Entscheidungen katastrophale Konsequenzen haben. Daher ist es von Interesse, maschinelles Lernen zu sichern. Hierfür sollen in einem symbolischen Zustandsraum Entscheidungen identifiziert werden, welche nicht sicher sind, und anschließend entfernt werden. |
|
Modellierung eines N-Battery Systems in DEMKit
|
Bachelor |
-
|
| Effizienzsteigerung durch Parallelisierung der Rückwärtsanalyse in RealySt |
Bachelor |
Das Tool RealySt (zum DFG Projekt RealySt) nutzt für die Analyse von Stochastischen Hybriden Automaten ein kombiniertes Verfahren aus Vorwärts- und Rückwärtsanalyse (Backward Refinement). Für die Vorwärtsanalyse wird hier die Library HyPro genutzt, die bereits eine parallelisierte Analyse anbietet. Entsprechend soll auch in RealySt die Rückwärtsanalyse parallelisiert werden. Momentan wird für die Methode bereits eine Task Queue genutzt, deren Elemente auch parallel abgearbeitet werden könnten. |
| Verbesserung der Erreichbarkeitsanalyse in RealySt durch den Einsatz von Zonotopen |
Master |
Die Erreichbarkeitsanalyse in unserem Forschungstool RealySt (zum DFG Projekt RealySt) nutzt momentan Polytope (in H- und V-Repräsentation) zur Darstellung von Zuständen. Im Rahmen einer Masterarbeit sollen Polytope in RealySt durch Zonotope ersetzt werden. Dafür müssen die Methoden und Datenstrukturen der Library HyPro geeignet genutzt werden. Abschließend sollen die beiden Ansätze in einer Case Study verglichen werden.
|
| Machine Learning zur Sicherung von SCADA-Systemen in zukünftigen Energieverteilungsnetzen |
Master |
Erneuerbare Energien werden über Kontrollnetzwerke mit dezentralisiertem Energie-Management bewacht, um einen stabilen Verteilungsprozess zu gewährleisten. Supervisory Control and Data Acquisition (SCADA) wird verwendet um Messungen zu kommunizieren und Befehle zwischen Komponentien auszutauschen. Zukünftige Energie-Verteilungssysteme werden eine höhere Konnektivität aufweisen und somit angreifbarer für Cyber-Angriffe sein. Es soll untersucht werden, inwieweit generative adverserial networks (GANs) verwendet werden können, um einen Datensatz mit gelernten Anomalien zu erzeugen. Diese Arbeit wird in Zusammenarbeit mit der Arbeitsgruppe von Prof. Risse betreut. |
| Entwicklung und Analyse smarter Ladestrategien für Plug-in Elektrofahrzeuge |
Master |
Es hat sich gezeigt das der Ladevorgang von Plug-in Electric Vehicles (PEVs) aufgrund der Batteriegröße und der Tendenz zu parallelen Lastzeiten eine große Belastung für das Stromnetz darstellt. Es gilt Ladestrategien zu entwickeln die, beispielsweise durch Koordination, das Powernetz entlasten. Gleichermaßen müssen solche Strategien ebenfalls sicherstellen, dass die PEVs möglichst vollständig geladen sind wenn der Besitzer zurückkehrt. In unserer Arbeitsgruppe wird modellbasiert das Laden von PEVs analysiert. Die Themen in diesem Arbeitsgebiet sind vielfältig. Generell geht es darum, relevante Ladestrategien in Modellen zu implementieren und deren Nutzen und Auswirkungen zu erforschen. Dabei ist vor allem die Betrachtung von vielen, gleichzeitigen Belastungen durch PEVs interessant. Hierfür sollen die theoretischen Grundlagen der Analysealgorithmen unserer Modelle erweitert werden. |
| Quantitative Analysis of Stochastic Simulink Models: A Case Study |
Bachelor |
- |
| A Modular and Extensible Parser for Simulink |
Bachelor |
- |
| Verbesserung der numerischen Integration in RealySt durch Monte Carlo basierter Vorverarbeitung |
Bachelor |
Das Open-Source-Tool RealySt berechnet optimale Erreichbarkeitswahrscheinlichkeiten für stochastische hybride Automaten. Diese Wahrscheinlichkeiten werden über eine mehrdimensionale Wahrscheinlichkeitsdichte numerisch integriert, wobei aktuell Monte Carlo Vegas verwendet wird. Ein neuer Ansatz ist, die numerische Integration durch eine Vorverarbeitung mit Stichproben aus einem Markov Chain Monte Carlo (MCMC)-Verfahren gezielt zu verbessern. Ziel dieser Arbeit ist es, diesen Ansatz in RealySt zu integrieren und zu untersuchen, ob sich dadurch Genauigkeit und Laufzeit der Integration verbessern lassen. Kenntnisse in C++ sind von Vorteil.
|
| Entwicklung und Bewertung skalierbarer Fallstudien für die Analyse stochastischer hybrider Automaten |
Bachelor / Master |
Fallstudien werden häufig eingesetzt, um Analysemethoden und deren Implementierungen in Tools miteinander zu vergleichen und deren jeweilige Stärken und Schwächen aufzuzeigen. Das Tool RealySt analysiert derzeit Modelle aus der Klasse der Rectangular Automata with Random Clocks (RAC) und validiert die Ergebnisse anhand bestehender Fallstudien gegen das Tool ProHVer.
Ziel dieser Arbeit ist es, mindestens eine neue, skalierbare Fallstudie zu entwickeln, die sich flexibel variieren lässt, z.B. durch alternative Modellklassen oder lineares Verhalten. Außerdem sollen existierende Fallstudien gesammelt, aufgearbeitet und bewertet werden. Eine Masterarbeit kann zusätzlich Herausforderungen bei der Modellierung und Analyse der neuen Fallstudie bearbeiten, während eine Bachelorarbeit stärker den Fokus auf existierende Literatur legt.
|
| Nutzung der Struktur von Wahrscheinlichkeitsverteilungen zur Optimierung der Erreichbarkeitsanalyse in RealySt |
Bachelor / Master |
Das Tool RealySt berechnet maximale Erreichbarkeitswahrscheinlichkeiten für Rectangular Automata with Random Clocks (RAC). Dabei wird die Struktur der zugrunde liegenden Wahrscheinlichkeitsverteilungen bislang jedoch nur für die konkrete Berechnung der Wahrscheinlichkeiten berücksichtigt – nicht gezielt während der Analyse selbst. Ziel dieser Arbeit ist es, Ansätze zu entwickeln und umzusetzen, die diese Struktur bereits im Analyseprozess gezielt ausnutzen. So könnten beispielsweise Pfade im Erreichbarkeitsbaum frühzeitig verworfen werden, wenn die aktuellen Einschränkungen für die Zufallsvariablen außerhalb relevanter Wahrscheinlichkeitsbereiche liegen. |
| Erweiterung von RealySt zur Expliziten Ausgabe der Scheduler Entscheidungen |
Master |
Im Rahmen unserer Forschung zu stochastischen hybriden Automaten sollen optimale Strategien (Scheduler) bestimmt werden, um Nichtdeterminismus gezielt aufzulösen. Das bestehende Tool RealySt berechnet bislang nur Erreichbarkeitswahrscheinlichkeiten solcher Systeme. Ziel dieser Arbeit ist es, RealySt so zu erweitern, dass zusätzlich die vom Scheduler getroffenen Entscheidungen explizit ausgegeben werden können. Die Arbeit umfasst die Analyse des bestehenden Ansatzes, die Konzeption einer geeigneten Ausgabeform sowie deren prototypische Implementierung. |
