Bei Interesse an einer Abschlussarbeit in der AG Embedded Systems schreiben Sie bitte eine E-Mail an julius.adelt@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:
-
Modeling Stochasticity in Simulink (jointly supervised with Prof. Anne Remke)
-
Automated Integration of Contracts into a SystemC to Timed Automata Transformation
-
Automating the Verification of Hybrid Contracts using Hybrid Automata
-
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)
-
Visualization of Large and Complex System Dependence Graphs
Beispielthemen für Masterarbeiten:
-
An Automated Transformation from Simulink to Hybrid Automata (jointly supervised with Prof. Anne Remke)
-
Advanced Information Flow Analysis for integrated Hardware/Software Systems
-
Formal Verification of an Intelligent Hexapod Robot using Differential Dynamic Logic (jointly supervised with Prof. Malte Schilling)
-
Model Monitoring / Conformance Testing for Verified Intelligent Hybrid Systems
-
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 Concurrent Embedded Systems with VerCors and Frama-C ( 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)
-
Optimizing a parallel Sorting Algorithm for Multi Robot Motion Planning (in Kooperation mit Prof. Dr. Christian Scheffer, Hochschule Bochum)