direkt zum Inhalt springen

direkt zum Hauptnavigationsmenü

Sie sind hier

TU Berlin

Inhalt des Dokuments

Zusätzlich zu den aufgeführten Themen können wir auch gerne weitere Themen anbieten. Also wenn ihr Interesse habt, kommt vorbei!
Kontakt: Verena Klös

Spezifikation und Verifikation von Echtzeitsystemen

Eingebettete Software wird oft in sicherheitskritischen Systemen, wie z.B. Autos und Flugzeugen eingesetzt. Dies bedeutet, dass ein Fehler des Systems zu hohen Kosten und unter Umständen zu Personenschäden führen kann. Um Fehler eines Systems ausschließen zu können, reichen Techniken wie Testen und Simulation inbesondere in Echtzeitsystemen nicht aus, da Randfälle leicht übersehen werden. Die formale Verifikation hingegen ermöglicht es, Fehler vollständig auszuschließen. Formale Verifikation kann jedoch nur angewendet werden, wenn die Modelle in einer Sprache vorliegen, die eine formale Semantik hat. Timed CSP ist eine solche formale Sprache zur Beschreibung nebenläufiger Echtzeit-Prozesse.

In diesem Themenbereich geht es darum, mit Varianten der Spezifikationssprache (Timed) CSP interessante und kritische Aspekte moderner eingebetteter Systeme zu modellieren und zum Teil zu analysieren. Der Fokus liegt dabei besonders auf nebenläufigen Multicore- oder adaptiven Systemen. Dabei wird nicht ausschließlich die Spezifikationsebene betrachtet sondern auch Implementierungen der Spezifikationen in z.B. der low-level Programmiersprache LLVM.


Mögliche Themen:

  • Modeling and analysis of multicore systems in Timed CSP
  • Modeling and analysis of adaptive systems in Timed CSP
  • Design patterns in CSP

Ansprechpartner: Thomas Göthel, Nils Jähnig

HW/SW Co-Verifikation

In den letzten Jahren haben wir am Fachgebiet SESE 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 Systembeschreibungssprache zur Anwendung und Evaluierung der entwickelten Techniken verwenden wir SystemC.

Bei SystemC handelt es sich um eine Modellierungssprache, die speziell für den Co-Entwurf von Hardware und Software entwickelt worden ist. SystemC ist als C++-Bibliothek implementiert und ermöglicht es HW/SW-Systeme über die Dauer des gesamten Entwurfs auf verschiedenen Abstraktionsebenen zu simulieren.

Aktuelle Beispielthemen:

  • Überdeckungsmessung für unvollständige Spezifikationen beim Model Checking temporallogischer Formeln
  • Timing Analysis für SystemC Designs
  • Automatische Partitionierung von HW/SW Systemen
  • Automatische Klassifikation von SystemC Designs
  • Automatische Klassifikation von PSL Eigenschaften

Ansprechpartner: Paula Herber

Refactorings hybrider Simulink Modelle

Simulink ist eine datenflussorientierte Sprache und Tool, das vor allem im Automobil- und Luftfahrzeugbereich weit verbreitet ist. Simulink wird dort verwendet, um Modelle für eingebettete Systeme zu erstellen. Dies ist notwendig, weil eingebettete Systeme heutzutage sehr komplexe Aufgaben zu bewältigen in der Lage sind, und man z.B. nicht einfach direkt die Software programmieren kann. Der Softwareentwickler oder auch der Regelungs-Ingenieur überlegen sich vielmehr zunächst abstrakt am Modell, wie das System sich später verhalten soll. Das Modell wird danach auch zur automatischen Codegenerierung genutzt.

Eine weitere wichtige Technik sind Refactorings. Das sind Modelltransformationen, also Veränderungen des Modells, mit folgenden Zielen:

  • Vereinfachung der Modelle
  • Herstellung der Konformität zu bestimmten Richtlinien.

Das Entscheidende, das eine Modelltransformation erfüllen muss, um sich als Refactoring zu qualifizieren ist, dass das Verhalten der Modelle vor und nach der Transformation äquivalent sein muss.

Was kann man sich nun konkret unter Refactorings vorstellen? Vereinfachungen könnten z.B. Entfernen von Clones (also mehrfachen Vorkommen desselben Musters) sein oder auch die Darstellung eines komplexen Feedbacksystems (oder Teilen davon) durch (Teil-)Lösungen. 

Richtlinien (wie die ISO 26262 in der Automobilindustrie) spielen vor allem in sicherheitskritischen Bereichen, also Gebieten, wo Leben in Gefahr ist oder ein Verlust einfach nicht hinnehmbar wäre, eine große Rolle. Dort stellt man verschiedene Kriterien an die Modelle, wie dass Blöcke nur über zwei Eingänge verfügen dürfen, nur bestimmte Datentypen zugelassen sind etc.

In sicherheitskritischen Bereichen spielt auch formale Verifikation, also mathematische Beweise des Wohlverhaltens der Modelle bzw. Programme eine große Rolle.

Die oben beschriebenen Stichworte umschreiben das Problemfeld, in dem in KorMoran Arbeiten vergeben werden können. Die Themen sind vor allem für Studenten interessant, die erste Erfahrungen mit Simulink sammeln möchten (oder bestehende Erfahrungen ausbauen wollen) - besonders interessant für Automobilindustrie und Luftfahrt - und ggf. auch an formaler Arbeit interessiert sind. Alle Themen sind nach Neigung der Studenten skalierbar, d.h. ist mehr Praxis bzw. Implementierung gewünscht, so lässt sich das einrichten. Wird dagegen mehr Theorie verlangt, ist auch das möglich.

 Beispielthemen:

  • Implementierung von interaktiven GUIs für einen Beweiser für die Verhaltensäquivalenz bei Refactorings in Java oder SCALA
  • Implementierung von Beweistechniken für die Verifikation von Refactorings

Speziell für den Luftfahrtbereich bieten wir darüber hinaus eine Kooperation mit dem Institut für Flugmechanik, Flugregelung und Aeroelastizität an der TU Berlin. Dort werden Arbeiten angeboten, die bestehende Simulink Refactorings verbessern sollen, Anpassungen für Datentypen vornehmen sollen etc.

Ansprechpartner: Sebastian Schlesinger

Analyse und Verifikation hybrider Simulink-Modelle

Simulink ist eine Systembeschreibungssprache und ein Tool, um eingebettete Systeme zu modellieren und simulieren. Über eine grafische Oberfläche werden Systeme über Blöcke und Signale zusammengesetzt. In den Blöcken werden Berechnungen durchgeführt, und über die Signale werden die Ergebnisse von einen Block zum nächsten weitergereicht.

In Simulink ist es möglich, Systeme zu modellieren, die sowohl diskretes Verhalten, wie sprunghafte Veränderung eines Wertes, als auch kontinuierliches Verhalten darzustellen, das zum Beispiel mit Differentialgleichungen beschrieben werden kann. Dies ermöglicht es, sogenannte hybride Systeme in Simulink zu modellieren und zu simulieren.

Wenn die Modelle für Anwendungen in sicherheitskritischen Bereichen wie im Automobilbereich oder in der Medizintechnik erstellt werden, spielt das korrekte Verhalten der erstellten Systeme eine besonders große Rolle. Jedoch reicht die in Simulink integrierte Simulation von Modellen allein nicht aus, um die Abwesenheit von fehlerhaftem Verhalten zu zeigen. Hierzu sind formale Methoden notwendig. Mit Analysen und Transformationen sollen Simulink-Modelle in ein Format überführt werden, das eine formale Verifikation ermöglicht.

In diesem Themenbereich werden mit Hilfe von Analysen und Transformationen Simulink-Modelle in eine Darstellung überführt, die eine formale Verifikation der Modelle ermöglicht. Mit einem service-orientierten Ansatz sollen Submodelle gefunden werden, die spezielle Funktionalitäten in einem Modell übernehmen. Durch eine allgemeine Darstellung der Services soll es ermöglicht werden die Services in anderen Modellen wieder zu verwenden und den Verifikationsaufwand durch bereits vorhandene Informationen zu reduzieren.

Beispielthemen:

  • Implementierung einer Abstraktion von Simulink-Modellen

Ansprechpartner: Timm Liebrenz

    Selbst-Adaptive Systeme mit adaptiver Adaptationslogik

    Selbst-Adaptive Systeme sind Systeme, die in der Lage sind, selbstständig auf Änderungen in der Umgebung, im System oder bezüglich der Systemziele, zu reagieren und sich bestmöglich anzupassen. Die Anpassung erfolgt in den meisten Fällen entsprechend einer vorgegebenen Adaptationslogik (z.B. Adaptationsregeln) und besteht z.B. darin zwischen vordefinierten Konfigurationen zu wechseln oder Systemparameter anzupassen.
    Eine solche statische Lösung ermöglicht schnelle Anpassungen, kann jedoch nicht bzw. kaum mit unvorhergesehenem Umgebungsverhalten umgehen, da in diesen Fällen die Adaptionslogik nicht angewendet werden kann oder Anpassungen nicht den gewünschten Effekt haben.
    Im Gegensatz dazu gibt es die Möglichkeit Adaptationsverhalten dynamisch zu lernen. Hierbei werden Lernverfahren aus der KI oder Model Checking verwendet.
    Da diese Verfahren mehr Zeit und Speicher benötigen als statische Regeln, untersuchen wir eine Kombination beider Verfahren, bei der Adaptationsregeln kontinuierlich evaluiert werden und ggf. unpassende Regeln deaktiviert und neue Regeln gelernt werden. Dies ermöglicht auch den Umgang mit Änderungen der Systemtopologie zur Laufzeit.

    Aktuelle Beispielthemen:

    • Evaluierung von Adaptationsregeln zur Laufzeit
    • Statische Adaptationsplanung unter Berücksichtigung von Abhängigkeiten und Zeit
    • Lernen und Korrigieren von Laufzeitmodellen des Systems
    • Lernen und Korrigieren von Laufzeitmodellen der Umgebung
    • Überwachung und Verwaltung der Systemtopologie
    • Entwicklung und Implementierung eines geeigneten Modells für Systemziele

     Ansprechpartnerin: Verena Klös

    Verifikation von Security Policies in Protected Binaries

    Die Digitalisierung der Gesellschaft, z.B. durch Trends wie das Internet of Things, führt zu einer Verzahnung unseres Alltages mit vielen vernetzten Geräten, sog. Cyber-Physical Systems. Die aktuelle Entwicklung zeigt dabei, dass gerade Geräte, mit denen wir in sensiblen Bereichen umgehen, häufig nicht die dafür eigentlich notwendige Sicherheit leisten können. Seien es Botnets, bestehend aus millionen von Webcams und intelligenten Küchengeräten oder auch smarte Fernseher, die heimlich in eine Abhörstation direkt im Wohnzimmer umfunktioniert werden: Die Möglichkeiten nehmen zu, die Bedrohungen auch.

    Damit die Nutzer den Systemen wieder vertrauen können, müssen sie sich selbst von deren korrektem Verhalten überzeugen können. Das ist jedoch leichter gesagt als getan. Die wenigsten Geräte werden mit Quellcode ausgeliefert, sodass eine Analyse auf dem ungleich komplexeren Maschinencode vorgenommen werden muss. Gleichzeitig kann beim Nutzer kein tiefgehendes Verständnis der Analyse von Hard- und Software vorausgesetzt werden. Der Prozess muss also automatisch anwendbar sein und in einem überschaubaren zeitlichen Rahmen korrekte Ergebnisse liefern.

    Wir forschen daher an Methoden mit denen auch komplexer Maschinencode auf die Korrektheit bezüglich einer Security Policy überprüft werden kann. In diesem Spannungsfeld spielen statische Programmanalyse, wiederherstellung des interprozeduralen Kontrollflusses und Verifikation durch Model Checking eine Rolle.

    Beispielthemen:

    • Implementierung einer statischen interprozeduralen Kontrollflussanalyse
    • Implementierung einer statischen Points-To-Analyse
    • Erstellung und Verifikation komplexer Beispiele zur Evaluation

    Ansprechpartner: Tobias Pfeffer

    Automotive System Engineering

    In Kooperation mit Assystem Germany bieten wir Abschlussarbeiten aus dem Bereich der Fahrzeugentwicklung an. Diese umfassen Themen aus aktuellen Projekten, die direkt im Hause Assystem in Berlin entwickelt werden.

    Themen:

    Ansprechpartner: Herr Uwe Becker (career (at) de.assystem.com)

     

     

    Zusatzinformationen / Extras

    Direktzugang

    Schnellnavigation zur Seite über Nummerneingabe

    Kontakt

    Verena Klös
    314 - 73451
    Raum TEL 1003