E-mail senden E-Mail Adresse kopieren

Verifikation der  SYSTEMGESUNDHEIT

LAUFZEITÜBERWACHUNG. AUTOMATISCHE PROGRAMMIERUNG ZUVERLÄSSIGER SYSTEME.

MOTIVATION

Automatisierte Systeme wie Autopiloten, unbemannte Flugzeugsysteme und selbstfahrende Autos sind von zunehmendem Interesse für eine Vielzahl von Anwendungen wie Logistik, Katastrophenhilfe und öffentliche Verkehrsmittel. Die Stabilität und Sicherheit dieser Systeme ist entscheidend für die Sicherheit ihrer Betriebsumgebung. Mit der Verifikation des Systemzustands stellen wir sicher, dass jeder Aspekt des Systems, von den Sensordaten bis hin zur autonomen Entscheidungsfindung, entweder nachweislich korrekt ist oder während der Laufzeit überwacht wird. Wir entwickeln Techniken, die Gegenmaßnahmen einleiten, bevor Unfälle passieren.

 

AKTUELLE FORSCHUNGSRICHTUNGEN

Laufzeitüberwachung von Cyber-Physikalischen Systemen. Cyber-Physikalische Systeme (CPS), wie medizinische Geräte und Drohnen, interagieren kontinuierlich mit ihrer unvorhersehbaren Umgebung. Während der Laufzeit haben solche Systeme oft mit enormer Unsicherheit zu kämpfen. Der Grund dafür, dass CPS versagen, liegt oft nicht an Implementierungsfehlern oder menschlichen Fehlern, sondern an unvorhergesehenen Ereignissen, die während des Betriebs auftreten. Mit der Laufzeitüberwachung von CPS setzen wir Sicherheitseinschränkungen für betriebliche Aspekte durch, die das Ausfallrisiko verringern.

Automatische Programmierung zuverlässiger Systeme. Sicherheitslücken können sehr subtil und tief in vielen Code-Schichten verborgen sein. Zum Beispiel ist ein unsicherer Informationsfluss, wie ein potentielles Leck von Kreditkarteninformationen, für die menschlichen Programmierer:in oft schwer zu erkennen. Bei der automatisierten Programmierung implementiert ein Computer anstelle eines Menschen die gewünschten Sicherheitsmechanismen im System. Wir entwickeln Techniken und Werkzeuge, die automatisch zuverlässige Systeme entwerfen.

Auf dem Weg zur formalen Zertifizierung. Wir konstruieren prägnante und umfassende mathematische Modelle von Systemen, die in einer unvorhersehbaren Umgebung sicher und zuverlässig interagieren. Auf der Grundlage dieser Modelle zertifizieren wir das Verhalten jeder Komponente, wie zum Beispiel der Sensortreiber oder der Flugsteuerung in einem unbemannten Flugzeugsystem. Wir entwickeln einen kompletten Werkzeugkasten für die formale Zertifizierung solcher Systeme.

LEAD FACULTY