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

Es gibt etliche Formalismen, die sich zur Modellierung (Spezifikation) and Analyse (Verifikation) von nebenläufigen Echtzeitsystemen eignen. Sie unterscheiden sich hinsichtlich ihrer Ausdrucksmächtigkeit und hinsichtlich der Aspekte eines Systems, die überhaupt erfasst werden können. So eignet sich z.B. Timed CSP sehr gut für die Modellierung prozessorientierter Aspekte wie Kommunikationsverhalten, während z.B. mit der Spezifikationssprache Z Datentypen und Operationen modelliert werden, welche von dem System verwendet werden.

In diesem Themenbereich geht es darum, mit Varianten der Spezifikationssprache (Timed) CSP interessante und kritische Aspekte moderner eingebetteter Systeme zu modellieren und (mit Toolunterstützung) 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 adaptation patterns in (Timed) CSP
  • Formalization and verification of parallel LLVM programs
  • Design patterns ins CSP

Ansprechpartner: Thomas Göthel, Nils Jähnig

Hardware/Software 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.

Beispielthemen:

  • Optimierung und Erweiterung einer Transformation von SystemC zu CPAchecker
  • Optimierung und Erweiterung einer Transformation von SystemC zu UCLID
  • Kompositionale Verifikation von integrierten HW/SW Systemen
  • Information Flow Analysis for SystemC

Ansprechpartner: Paula Herber

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 Transformation von Statflow-Modellen in Differential Dynamic Logic

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:

  • Kompositionale Verifikation adaptiver Systeme

 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:

  • Erweiterung eines multi-execution Frameworks
  • Noninterferenceanalyse von symbolic traces

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:

    • Systematische Modellierung von IIoT Anwendungen, insbesondere der Kommunikation
    • Automatische Generierung der IP-basierten Kommunikationsarchitektur (Configuration Mapping)

    Ansprechpartner: Benjamin Feldner, Paula Herber

    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