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

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.


Beispielthemen:

  • NEU Abstract representations of processes NEU
    Design heuristics to generate sufficient conditions from CSP processes to relate CSP processes and executable programs.
  • 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

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:

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

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.

    Beispielthemen:

    • Lernen und Korrigieren von Laufzeitmodellen des Systems und der Umgebung

     Ansprechpartnerin: Verena Klös

    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

    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.

    Beispielthemen:

    • Evaluierung von Modellbasierten Entwicklungsansätzen im Bereich IIoT
    • Entwicklung eines Webbasierten Modellierungswerkzeug für IIoT Anwendungen
    • Entwicklung von Proxy-Komponenten für proprietäre Protokolle wie z.B. Modbus, I/O Link
    • Systematische Migration von IPv4 zu IPv6 für bestehende IIoT Anwendungen
    • Entwicklung von IIoT Anwendungen als Fallstudien

    Ansprechpartner: Benjamin Feldner

    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

    Joachim Fellmuth
    314 - 24789
    Raum TEL 1007