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: Joachim Fellmuth

Design 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:

  • Integrierung von Feature Modeling in Simulink
  • Implementierung einer Simulink Case-Study mit Verwendung einer Service-Orientierten Modellierung

Ansprechpartner: Timm Liebrenz

    Verifikation der Security Eigenschaften von Maschinencode

    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 gewärleisten 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 Einhaltung von Sicherheitsrichtlinien, wie z.B. Vertraulichkeit von Information, überprüft werden kann. In diesem Spannungsfeld behandeln wir statische und dynamische Programm- und Verhaltensanalysen, wie z.B. Self-Composition oder Symbolic Execution.

    Beispielthemen:

    • Implementierung einer post-mortem Informationsflussanalyse
    • Erweiterung eines multi-execution Frameworks
    • Statische Verhaltensanalyse für I/O via Symbolic Execution

    Ansprechpartner: Tobias Pfeffer

    Security mit Artificial Software Diversity in Echtzeitsystemen

    Cyber-Physical Systems (CPS) haben einen immer größer werdenen Einfluss auf unser Leben, da immer mehr Systeme durch Computer gesteuert werden, die untereinander stark vernetzt und auch mit dem Internet verbunden sind. Unter diesen Systemen sind auch harte Echtzeitsysteme wie Airbags und ABS Controller, bei denen verpasste Zeitschranken als Systemversagen gewertet werden. Wenn eine solche Systemfunktionalität sicherheitskritisch ist, z.B. das Auslösen des Airbags, muss der Entwickler Sicherheits- und Zeitgarantien liefern.

    Wenn sicherheitskritische Systeme potentiellen Angreifern ausgesetzt sind, gehören zu den Sicherheitsgarantien auch Themen aus dem Bereich Security. Besonders Kontrollflussattacken sind eine Gefahr für CPS. Bestehende Ansätze zum Schutz können, z.B. wegen begrenzten Ressourcen und Betriebssystemfunktionalitäten, aktuell oft nicht angewandt werden oder sind nicht wirksam genug.

    Unsere Arbeit beschäftigt sich mit der Entwicklung von Methoden, durch die Artificial Software Diversity, ein nachgewiesen wirksamer Schutz gegen viele Angriffe, auch in sicherheitskritischen Echtzeitsytemen zum Einsatz kommen kann. Dabei arbeiten wir mit Analyse und Manipulation von Low-level Code Repräsentationen, wie Assembler, aber auch mit verschiedenen Aspekten der statischen Worst-Case-Execution-Time (WCET) Analyse.

    Beispielthemen:

    • Entwicklung eines Diversity-Ansatzes zur Load-Time für Echtzeitsysteme
    • Erweiterung von bestehenden statischen WCET Analysen für Caches und Sprungvorhersage, so dass sie Diversity unterstützen

    Ansprechpartner:

    Modellbasiertes Deployment von Industrial Internet of Things Anwendungen

    Zurzeit bieten wir zu diesem Themenbereich keine Abschlussarbeiten an.

    Mit der zunehmenden Vernetzung von eingebetteten Systemen, zum Beispiel im Zusammenhang mit Smart Factories und Industrie 4.0, gewinnen "Industrial Internet of Things" (IIoT) Anwendungen immer mehr an Bedeutung. IIoT Anwendungen werden in der Industrie zum Beispiel eingesetzt um verteilte Anlagen in der Fertigung zu vernetzen und zu überwachen.

    Zur methodischen Erstellung solcher IIoT-Anwendungen gibt es jedoch weitaus weniger computergestützte Entwurfswerkzeuge, als dies z.B. für konventionelle Applikationen der Fall ist. Existierenden Ansätze im Bereich der modellbasierten Entwicklung fokussieren meist auf die Funktionalität der Anwendung und lassen das grundlegende Kommunikationssetup, die Integration bestehender Kompononenten mit teilweise proprietären Protokollen und das Deployment der Anwendung aussen vor.

    Vor diesem Hintergrund wird in Kooperation zwischen dem Fachegebiet SESE an der TU Berlin und einem externen Doktoranden, der bei HARTING IT Software Development tätig ist, ein Framework entworfen, das die Entwicklung von IIoT-Anwendungen modellgestützt vereinfacht und Phasen im Software Lifecycle soweit möglich automatisieren soll. Die Informationen aus dem abstrakten Modell sollen für konkrete Anwendungen genutzt werden, um grundlegende IP-basierte Kommunikationsfähigkeit möglichst automatisch herzustellen (Configuration Mapping). Darüber hinaus soll das Deployment der gesamten Anwendung automatisch ermöglicht werden.

    Ansprechpartner: Benjamin Feldner

    Zusatzinformationen / Extras

    Direktzugang

    Schnellnavigation zur Seite über Nummerneingabe

    Kontakt

    Joachim Fellmuth
    314 - 24789
    Raum TEL 1007