Bei Interesse an einer Abschlussarbeit in der AG Embedded Systems schreiben Sie bitte eine E-Mail an pauline.blohm@uni-muenster.de
Abschlussarbeiten in der AG Embedded Systems
In den letzten Jahren haben wir aus der AG Embedded Systems verschiedene Techniken zur HW/SW Co-Verifikation entwickelt, unter anderem zum Model Checking und zum Testen von HW/SW Systemen. In diesem Bereich haben wir ständig verschiedene Bachelor- und Masterarbeiten zu vergeben. Als beispielhafte Systembeschreibungssprachen zur Anwendung und Evaluierung der entwickelten Techniken verwenden wir SystemC und Simulink, beide Sprachen stammen aus dem industriellen Kontext.
Bei SystemC handelt es sich um eine Modellierungssprache, die von einem Industriekonsortium für den Co-Entwurf von Hardware und Software entwickelt wurde. SystemC ist als C++-Bibliothek implementiert und erweitert C++ um Konstrukte zur Beschreibung von Hardware, also z.B. Zeit, Reaktivität und Parallelität. SystemC ermöglicht es, integrierte Hardware/Software-Systeme über die Dauer des gesamten Entwurfs auf verschiedenen Abstraktionsebenen zu modellieren und zu simulieren.
Die Modellierungssprache Matlab/Simulink ist eine datenfluss- bzw. signalflussorientierte Sprache zur Modellierung und Simulation komplexer dynamischer Systeme. Simulink ist als eine Erweiterung klassischer Blockdiagramme implementiert, wobei die Signale, die Blöcke verbinden, sowohl kontinuierlich als auch diskret sein können und die Blöcke komplexe mathematische Funktionen umsetzen, z.B. Integratoren, Sinuskurven oder Transformationsfunktionen, es lassen sich also auch komplexe Differential- und Differenzengleichungssysteme modellieren.
Beispielthemen für Bachelorarbeiten:
-
Quantitative Analysis of Stochastic Simulink Models: A Case Study (jointly supervised with Prof. Anne Remke)
- A Graphical Editor / Graphical User Interface for Stochastic Hybrid Automata
- Information Flow Analysis for Timed, Concurrent Systems: A Case Study
-
Visualization of Large and Complex System Dependence Graphs
-
Verifiable Implementation of RTOS-based Software: A Case Study (in cooperation with the Formal Methods and Tools (FMT) group of the University of Twente)
-
Find my invariant: Automatically infer Loop Specifications in Embedded Systems (in cooperation with the Formal Methods and Tools (FMT) group of the University of Twente)
-
An Automated SystemC-to-C Transformation for Deductive Verification with Frama-C (in cooperation with the Formal Methods and Tools (FMT) group of the University of Twente)
-
A Comparison of Frama-C and VerCors for the Deductive Verification of an Anti-lock Braking System (in cooperation with the Formal Methods and Tools (FMT) group of the University of Twente)
Beispielthemen für Masterarbeiten:
-
Quantitative Analysis of Intelligent Simulink Models using Hybrid Automata (jointly supervised with Prof. Anne Remke)
-
Combining Quantitative Analysis and Deductive Verification for Stochastic Simulink Models (jointly supervised with Prof. Anne Remke)
-
Efficient Information Flow Analysis for Timed, Concurrent Systems
-
Context Sensitive Information Flow Analysis for Timed, Concurrent Systems
-
Heuristic Abstraction Refinement for Information Flow Analysis
-
Metamorphic testing for machine learning based ECG classification (in Zusammenarbeit mit BIOTRONIK Berlin)
-
Using reinforcement learning to search for mission-critical test cases in satellite on-board image processing (in Zusammenarbeit mit dem Institute of Optical Sensor Systems des Deutschen Zentrum für Luft- und Raumfahrt (DLR) im Kontext der PLATO Mission der European Space Agency (ESA))
-
Deductive Verification of RTOS-based Embedded Systems with VerCors ( in cooperation with the Formal Methods and Tools (FMT) group of the University of Twente)
-
Automated Invariant Generation for Scalable Verification of SystemC Designs ( in cooperation with the Formal Methods and Tools (FMT) group of the University of Twente)