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 Modular and Extensible Parser for Simulink

  • Information Flow Analysis for Timed, Concurrent Systems: A Case Study

  • Visualization of Large and Complex System Dependence Graphs

  • Verifiable Implementation of RTOS-based Software on real Hardware: 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)

Beispielthemen für Masterarbeiten:

  • Combining Quantitative Analysis and Deductive Verification for Stochastic Simulink Models (jointly supervised with Prof. Anne Remke)

  • Optimized Automated Transformation from Simulink to Stochastic Hybrid Automata

  • 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)

  • Automated Invariant Generation for Scalable Verification of SystemC Designs ( in cooperation with the Formal Methods and Tools (FMT) group of the University of Twente)

 

Laufende Arbeiten

  • 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))

  • A Graphical Editor / Graphical User Interface for Stochastic Hybrid Automata

  • Statistical Analysis of a Walking Hexapod Robot modeled Simulink

  • Quantitative Analysis of Intelligent Simulink Models using Hybrid Automata (jointly supervised with Prof. Anne Remke)

  • Optimizing a parallel Sorting Algorithm for Multi Robot Motion Planning (Masterarbeit in Kooperation mit Prof. Dr. Christian Scheffer, Hochschule Bochum)

Abgeschlossene Arbeiten

  • Towards Formal Analysis of Uncertainty in Simulink using Stochastic Hybrid Automata (Bachelor Thesis, 2025)

  • Safe Model-Driven Design using Simulink2SHA: A Case Study (Bachelor Thesis, 2025)

  • RTOS2UPPAAL: Automated Transformation from Real-Time Applications into Timed Automata (Master Thesis, 2025)

  • Safety Standard Compliance in Embedded Systems using Dual-Core Processors for Redundancy (Masterarbeit in Kooperation mit der Völkel Mikroelektronik GmbH)

  • A Literature Study on Information Flow Analysis of Timed and Concurrent Systems (Bachelor Thesis, 2024)

  • Automated Integration of Contracts into a SystemC to Timed Automata Transformation (Bachelor Thesis, 2024)

  • Modellierung von Adaptiven, Intelligenten Hybriden Systemen in Simulink: Eine Fallstudie (Bachelor Thesis, 2023, jointly supervised with Prof. Malte Schilling)

  • A literature study on explainable genetic algorithms (Bachelor Thesis, 2023)

  • System Dependence Graph Construction for Information Flow Analysis in SystemC (Bachelor Thesis, 2023)

  • Deductive Verification of Resilience in Hybrid Intelligent Systems (Master Thesis, 2023)

  • An Abstract Model of an Intelligent Hexapod Robot in Simulink (Bachelor Thesis, 2023, jointly supervised with Prof. Malte Schilling)

  • Verification of an Anti-lock Braking System modeled in SystemC with Frama-C (Bachelor Thesis, 2023, in cooperation with the Formal Methods and Tools (FMT) group of the University of Twente)
  • A Comparison of Multi-Robot Motion Planning Algorithms (Bachelor Thesis, 2023, in Kooperation mit Prof. Dr. Christian Scheffer, Hochschule Bochum)
  • Information Flow Analysis for integrated Hardware/Software Systems  (Master Thesis, 2023)
  • Modeling Resilient Hybrid Systems in Simulink (Bachelor Thesis, 2023)
  • An explainable/domain-specific genetic algorithm to search for mission-critical test cases in satellite on-board image processing (Master Thesis, 2023, 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))
  • Automating the Verification of Hybrid Contracts with the Simulink Design Verifier (Bachelor Thesis, 2023)
  • An Evaluation Framework for Multi-Robot Motion Planning Algorithms (Bachelor Thesis, 2022, in Kooperation mit Prof. Dr. Christian Scheffer, Hochschule Bochum)

  • Safe use of Machine Learning in integrated Hardware/Software Systems (Master Thesis, 2022)

  • Automated Integration of Hybrid Contracts into Formal System Models with Simulink2dL (Bachelor Thesis, 2022)

  • Simulation of an Autonomous Robot in Gazebo: A Case Study (Bachelor Thesis, 2022)

  • Model-based Testing of complex Messages in Biomedical Applications (Masterarbeit in Kooperation mit dem Medizin-Geräte-Hersteller BIOTRONIK, 2022)

  • Reusable Hybrid Contracts for Deductive Verification of Intelligent Hybrid Systems (Master Thesis, 2022)

  • Modeling and Verification of Autonomous Robots with Hybrid Automata: A Case Study (Bachelor Thesis, 2022)

  • Literature Study: Symbolic Reinforcement Learning for Intelligent Control (Bachelor Thesis, 2022)

  • From Simulink to Hardware: A Case  Study with Smart Warehouse Robots (Bachelor Thesis, 2022)

  • Verification of Embedded Systems running with the Real-time Operating System EV3RT (Master Thesis, 2022)

  • Automated Testing for SLAM - Simultaneous Localization and Mapping (Master Thesis, 2021) 

  • Automated Transformation and Verification of integrated Hardware/Software systems with the VerCors Verification Tool (Master Thesis, 2021, in cooperation with the Formal Methods and Tools (FMT) group of the University of Twente)

  • Transformation from combined Simulink/Stateflow models to differential dynamic logic (Master Thesis, 2021)

  • Verifiable intelligent Cyber-Physical Systems: A case study in Simulink with the Robotics System Toolbox (Bachelor Thesis, 2021)

  • Traffic Flow Management in Simulink: A Case Study (Bachelor Thesis, 2021)
  • Verifying a Reinforcement Learning Controller with Simulink and KeYmaera X (Bachelor Thesis, 2021)
  • Error detection capability of a test partitioning approach for satellite on-board image processing (Bachelorarbeit (2021) in Kooperation 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))
  • Reinforcement Learning in SystemC: A Case Study (Bachelor Thesis, 2021)
  • Verifying intelligent cyber-physical systems with the interactive theorem prover KeYmaera X (Master Thesis, 2020)
  • Early Security Analysis in SystemC: Modeling and Simulation of Non-Invasive Physical Attacks (Master Thesis, 2020)
  • Optimierte Routenplanung für autonome Rasenmähroboter mithilfe genetischer Algorithmen (Bachelorarbeit in Kooperation mit der Arobo GmbH, 2020)
  • Linear routing optimization for lawn-mowing robots (Bachelor Thesis, in cooperation with Arobo GmbH, 2020)
  • Modelling Cache Attacks in SystemC (Bachelor Thesis, 2020)
  • Modeling and Simulation of IoT-Protocols in SystemC - A Smart Street Light System (Bachelor Thesis, 2020
  • Simulation of Lego Robots in SystemC: A Case Study (Bachelor Thesis, 2020)
  • Modellierung und Simulation eines Echtzeitbetriebssystems in SystemC (Bachelorarbeit, 2020)
  • Machine Learning based Load Forecasting for Peak Shaving in an Energy Management System (Bachelor Thesis, in cooperation with Fraunhofer Institute for Solar Energy Systems ISE, 2020)
  • Aktuelle Forschung zu IoT-Protokollen: eine Literaturstudie (Bachelorarbeit, 2020)
  • Automated Formal Verification of Hardware/Software Co-Designs with UCLID 5 (Bachelor Thesis, 2019)
  • Evaluation: Verifying SystemC designs with the CPAchecker (Bachelor Thesis, 2019)
  • Reinforcement Learning for Safety-Critical Systems: A Literature Review (Bachelor Thesis, 2019)
  • Modeling and Simulation of IoT Protocols in SystemC: MQTT and HTTP (Bachelor Thesis, 2019)
  • Modeling CoAP and XMPP in SystemC (Bachelor Thesis, 2019)
  • Modeling Power Analysis Attacks in SystemC (Bachelor Thesis, 2019)
  • A Survey of Development Frameworks used for IoT Applications (Bachelor Thesis, 2019)