We supervise theses in the following areas:

• Symbolic model checking and -execution Dimitri Bohlender, M.Sc. RWTH
• Static analysis Hendrik Simon, M.Sc.
• Formal methods for PLC programs Marcus Völker, M.Sc. RWTH
• Synthese von Steuerungssoftware: Florian Göbe, M.Sc. RWTH
• Unterstützung des Entwicklers während der Eingabe: Mathias Obster, M.Sc. RWTH
• Modeling/specification & analysis of embedded component systems Marc Förster, M.Sc.
• (Semi-)Formal Methods for Hazard Anaylsis & Risk Assessment according to ISO 26262 Paul Chomicz, M.Sc.

* Embedded Systems in Medicine:

• Safety in Medical Applications: Dr.-Ing. André Stollenwerk
  
• Eingebettete Systeme zur Kommunikation und Überwachung in der Intensivmedizin: Dipl.-Ing. (FH) Jan Kühn, M.Sc.
• Validierung der hygienischen Händedesinfektion zur Vermeidung nosokomialer Infektionen: Manfred Smieschek, M.Sc. RWTH
• Nutzung mobiler Plattformen für Hardware-in-the-Loop Tests & Verbesserung der Echtzeitfähigkeit von Kommunikationsmedien: David Thönnessen, M.Sc. RWTH
• Driver Assistance for Electric Wheelchairs Dzenan Dzafic, M.Sc. RWTH
• Model-based Testing for automobile Software Dipl.-Inform. Norbert Wiechowski

In case of interest, please contact the respective scientific researcher directly.

The following list is possibly not complete. You can directly ask the scientific researchers for additional proposals.

• eNav – Collision-Avoidance System for electric wheelchair
• CiTi - Generation of simulation models for Vissim via aerial photographs
• CiTi - Generation of traffic models for Vissim
• eNav - eNav Software´s quality management
• Insel-Spezifikationen für ein Tool zur Steuerungs-Synthese
• Automatisiertes Testen einer ECMO-Regelung
• Evaluation eines Werkzeugs zur Supervisorsynthese auf einer prozesstechischen Anlage
• Optimierung des Prozessverhaltens auf Real-Time Android
• Weiterentwicklung einer statischen Analyse für Simulink-Modelle
• Statische Analyse von Matlab/Simulink Stateflow-Charts
• Spezifikationsanalyse für Echtzeitsysteme
• Bounded Model Checking of Programmable Logic Control Software
• Coverage testing for composite function block diagrams
• Eingabeunterstützung für kontrollierte Sprachen

The following list is possibly not complete. You can directly ask the scientific researchers for additional proposals.

• eNav – Collision-Avoidance System for electric wheelchair
• CiTi - Generation of simulation models for Vissim via aerial photographs
• CiTi - Generation of traffic models for Vissim
• eNav - eNav Software´s quality management
• Qualitätssicherung der Systemkonfiguration von Real-Time Android
• Analyse von sicherheitskritischen Modellen für Tilt-wing Anwendungen
• Entwurf und Implementierung eines Repositorys für die automatisierte Testplanung von sicherheitskritischer eingebetteter Software
• Weiterentwicklung einer statischen Analyse für Simulink-Modelle
• Spezifikationsanalyse für Echtzeitsysteme
• symbolischemethoden
• Deduktive Programmsynthese für SPS-Funktionsblöcke
• Bounded Model Checking of Programmable Logic Control Software
• Coverage testing for composite function block diagrams

• eNav - Evaulation of eNav-Systems from users study

* eNav – Collision-Avoidance System for electric wheelchair

• Entwicklung einer konsistenten A*-Heuristik für das eNav-Routing
• eNav - Optimal subsets of point of interest
• Ansteuerung von SPS-Timern und erweiterte Codegenerierung für ein Werkzeug zur Synthese von ereignisdiskreten Überwachern
• Qualitätssicherung der Systemkonfiguration von Real-Time Android
• Inkrementelle Analyse für Steuerungscode
• Automatisiertes Testen im medizintechnischen Bereich
• Eingebette Rezirkulationsmessung für ECLA-Systeme
• Editor und Steuerungsapplikation für pulsatile Blutflüsse
• Fahrbahnoberflächen-Erkennung zur Optimierung von GPS-Positionsbestimmungen
• Nutzung eines Smartphone-Inertialsensors und Odometrie zur Optimierung von GPS-Positionsbestimmungen
• Datenbankbasierte Eingabeunterstützung für Gefährdungsanalysen

• CERM - CERM data management via Ros
• eNav - Development of a remote control for a wheelchair
• eNav development using PostgreSQL and evaluation
• CiTi - Generation Automatic Simulation for Vissim
• Grammatikkonforme Eingabeunterstützung
• Vergleichseditor für Gefährdungsanalysen
• Semi-automatische Übersetzung von alten Gefährdungsanalysen

• eNav Entwickelung auf Basis von Neo4j
• eNav - Integration of ÖPNV in eNav
• Verwaltungssystem für kontrollierte Sprachen
• Visueller Editor für Gefährdungsanalysen
• Grammatik für die Formalisierung von Exposure Rationales und semiautomatisierte Einstufung des Exposure Parameters
• Konsistenzprüfung von Gefährdungsanalysen

• Entwicklung einer Client-Server-Anwendung zur Verwaltung hygienerelevanter Daten im Krankenhausalltag
• Evaluation verschiedener drahtloser Übertragungsstandards zur intelligenten Lokalisation und Identifikation
• Integration einer Komponente zum Melden von Barrieren in das eNav System
• Automatisiertes Ermitteln von Öffnungszeiten als Erweiterung für das eNav System
• Code-Generator und Framework für synthetisierte Sicherheitsmechanismen in SPS-Programmen
• Anforderungsanalyse und prototypische Umsetzung einer Entwicklungsumgebung für Structured Text auf RTAndroid
• Sicherheitsorientierte Beatmungsansteuerung
• Erkennung von Bodenbelägen mithilfe eines Smartphones

• Evaluation von Synthesetools für Steuerungssoftware im Bereich der Automatisierungstechnik
• Rezirkulationsmessung bei extrakorporaler Lungenunterstützung
• Entwicklung mobiler Multiplattform-Clients für ein Buchungssystem
• Thermodynamische Modellbildung eines Handdesinfektionsprozesses
• Tiefeninformationsabhängige Bildfusion in einer optischen Desinfektionsvalidierung
• Implementierung von eingebetteter stereoskopischer Triangulation für einen 3D-Scanner
• Erarbeitung einer Ansteuerungsautomatik für eine Unabhängige Energieversorgung
• Funktionale Erweiterung des VMware vSphere Systems
• Erarbeitung einer mikrowellengeregelten chemischen Reaktionsführung
• Auslegung einer pulsatilen Ansteuerungsstrategie für eine Blutpumpe
• Entwicklung einer HTML5-basierten Schnittstelle für das mobile Navigationssystem eNav
• Integration von Informationen über die Bodenbeschaffenheit in das eNav System
• Entwicklung einer Simulations- und Debuggingumgebung für Bilderkennungsverfahren im Bereich autonomer Mobilität
• Portierung einer Diagonalpumpensteuerung auf ein eingebettetes Betriebssystem mit Unterstützung modell-basierter Sicherheitsmaßnahmen
• Modellierung und Analyse von konkurrierenden Sicherheitszielen in einer intensivmedizinischen Anwendung

• A conceptual framework and tool for ISO 26262 compliance
• Flexible Konfiguration eines mikrocontrollerbasierten Feldgeräteadapters für RTAndroid
• Entwicklung eines Testframeworks für Lebenszyklus‐Eigenschaften mobiler Applikationen
• Ausführung und Simulation von SPS-Programmen auf RTAndroid
• Inkonsistenz-Management von Artefakten in der modellbasierten Entwicklung eingebetteter Software
• Evaluierung von formalen Methoden in der Softwareentwicklung von kleinen und mittleren Unternehmen

• Modulare und Boolesche Abstraktion von SPS-Programmen
• Specifying Life Cycle Requirements for mobile Applications
• Integration des eNav Routing Algorithmus in einen OSM Server
• Entwicklung eines Versuchsaufbaus zur optischen Desinfektionsvalidierung
• Erarbeitung und Integration von modellbasierten Sicherheitsmaßnahmen für eine intensivmedizinische Anwendung
• Portierung einer Diagonalpumpensteuerung auf ein eingebettetes Betriebssystem mit Unterstützung modell-basierter Sicherheitsmaßnahmen
• iOS-Extension to the Higgs Framework
• Test und Stabilisierung von RTAndroid
• Steuerung einer Fertigungsanlage mit RTAndroid
• Reverse Engineering des Windows Phone Process Execution Models
• Interactive Visualization of Telecommunication Protocol Specs
• Sichere Überquerung einer Kreuzung mit einer Fahrzeugkolonne
• Effiziente Überquerung einer ampelgesteuerten Kreuzung mit einer Fahrzeugkolonne
• Entwurf und Validierung einer auf den Wirkungsgrad optimierten Regelungsstrategie zur Ansteuerung einer piezoelektrisch betriebenen Pumpe für automobile Anwendungen
• Optimierung einer oktagonbasierten Wertebereichsanalyse durch Lokalisierung abstrakter Speicherstellen
• Integration von Hardwareabstraktion und Hardwareansteuerung im eingebetteten Echtzeitbetriebssystem ChibiOS
• Concept and Prototype of a Mobile Cross-Device Test Framework
• Erstellung und Evaluation einer Hardwareplattform zur präzisen Ladezustandserfassung von Blei-Gel-Akkumulatoren
• Realisierung eines modellbasierten Annotationskonzepts für die Verknüpfung von Prozessartefakten

• Werkzeuggestützte Implementierung eines Simulators für Renesas R8C/Tiny-Mikrocontroller zur Erweiterung des Model-Checkers [mc]square
• Statische Analyse von Speicherprogrammierbaren Steuerungen (PLCs)
• S7 Simulator für [mc]square
• Erweiterung eines Tools zur Analyse von Lebenszyklusmodellen von Android-Applikationen
• Modellierung und Regelung des Blutflusses einer Diagonalpumpe bei der extrakorporalen Oxygenierung
• Unterstützung eines fahrzeuginternen Ortungssystems durch Sensorfusion
• Design and Integration of Real-Time into the Android Platform
• Development of an Autonomous Flight Control System for Micro Aerial Vehicles
• Untersuchung der Anwendbarkeit von Timed Hierarchies innerhalb der Signaltechnik
• Entwicklung eines Zeitsynchronisationsverfahrens für ein intensivmedizinisches, verteiltes System
• Analyse von Lebenszyklusmodellen mobiler Anwendungen
• Testing Lifecycle Implementations of Mobile Applications
• Entwicklung und Evaluierung eines Navigationssystems für Elektromotoren
• Analyse von hardwarenahen C-Programmen mit Oktagonen

• Entwicklung eines dezentral implementierten Sicherheitskonzeptes für intensivmedizinische Anwendungen
• Statische Analyse von Mikrocontrollerprogrammen mittels SAT- und Constraint-Solving
• Implementierung eines Simulators für Renesas-Mikrocontroller
• Transformation abstrakter Verhaltensmodelle von Regelstrecken
• Verifikation der Java Echtzeitfähigkeit für den Einsatz in zeitkritischen Systemen
• Synthese eines Befehlssatz-Simulators für das Model-Checking von Software für eingebettete Systeme
• Entwicklung einer Metrik zur Bewertung verschiedener Hardwareplattformen für medizintechnische Anwendungen
• Entwicklung und Spezifikation eines CAN Protokolls für sicherheitskritische medizintechnische Anwendungen
• Untersuchung des Potentials des Variabilitätsmanagements in der modellbasierten Software-Entwicklung

• Implementation of a Simulator for a Renesas Microcontroller
• Static Analysis of Microcontroller Software using SAT- and Constraint-Solving
• Transforming Abstract Behavior Models of Control Paths
• Synthesizing an Instruction Set Simulator for Model Checking Embedded Systems Software
• Examining the Potential of Variability Management in Model-Based Software Development
• Verification of the Java Real-Time Capability for the Application in Time-Critical Systems
• Development of a safety-critical CAN Protocol for a medical application
• Development of a Metric for the Evaluation of Different Hardware Platforms with Respect to a Safety-Critical Medical Application

• Application of Static Analysis in the Field of Model Checking Software for Embedded Systems
• Model Checking Abstract State Machines with [mc]square
• Parallel and Distributed Construction of the State Spaces in the Model Checker [mc]square
• Application of the Rasch Model for Quantitative Determination of Programming Experience
• Evaluating Temporal Source Code Modification Using Latent Semantic Indexing
• Development and Validation of Variables for Progress-Determination of a Controlled Experiment's Software
• Design of an Interactive Web-System for Gaining and Presenting Expert Knowledge in the Area of Embedded Systems
• Design and Development of a Modular Test and Simulation Environment for Automotive Applications
• Evaluating the Software Architecture of a Rapid-Control-Prototyping System for Engine Management Systems
• Extending the Model Checker [mc]square to Handle the Infineon XC167 Microcontroller
• Extending the Model Checker [mc]square by User-Defined Environments
• Extending the Symbolic Representation of States in [mc]square
• Integrating Hardware-Error-Tolerance-Mechanisms in Safety-Critical Systems
• Model-Checking of Instruction List Programs for Programmable Logic Controllers using [mc]square
• Model-Checking of Sensor Network Nodes with the Help of [mc]square
• Software Design Patterns and Functional Safety
• Symbolic Model Checking in [mc]square
• Comparison of Alternative Hardware-Architectures for Safety-Critical Automotive Applications
• Analysis of a MCU+FPGA architecture for safety critical automotive applications according to ISO 26262
• Analysis of a Dual-Core microcontroller for safety critical automotive applications according to ISO 26262
• Visualization of Source Code Evolution
• Line-Based Source Code Analysis in the Course of Time

• An Approach for Model Checking Embedded Systems Software
• Concept and Implementation of a Fault Management Framework for a dependable in-vehicle E/E-architecture
• Studies on the Application Potential of Formal Verification in the Engine Management Systems Software Domain
• Experiment on the Applicability of Refactoring on Embedded System Software Engineering
• Design and Implementation of a Drive-by-Wire Architecture
• The Effects of Refactoring on Embedded Systems Software Engineering
• Designing and Implementing a Software Watchdog for Fault-Tolerant Automotive Safety Electronics
• Design of Safety-Critical Embedded Systems using Design Patterns
• Analysis of Alternative Hardware Architectures in Embedded Systems Regarding Safety and Reliability
• Design and Integration of an Autonomous Parking Assistant in an Experimental Vehicle for Automotive Software
• A Component Model for Embedded Systems

• Requirements for a Model Checker for Matlab/Simulink
• Design of an Assistance Tool/Framework for Code-Evolution Experiments
• Development of a Web-Based Tool for the Assistance in Code-Readability Experiments
• Evaluation of a CASE-Tool for Embedded Systems
• A Description Language for Rich Component Models in Automotive Software
• Conception and Implementation of an Experimental Vehicle for Automotive Software
• Collection and Comparison of Design Principles Considering Technology-Independent Modelling in the Automobile Industry
• Selection and Implementation of a HW/SW Co-Design Environment
• Design and Implementation of the Speed Measurement in a Vehicle Prototype applying the IEC 61508
• PLD Programming for Safety-Relevant Embedded Systems
• Research on the Distributability of Software-Functionalities in a Total-Vehicle-Architecture