direkt zum Inhalt springen

direkt zum Hauptnavigationsmenü

Sie sind hier

TU Berlin

Page Content

Available subjects for bachelor theses or term projects are listed below. We also can offer subjects not listed here, depending on your interests. Feel free and visit us.
Contact: Joachim Fellmuth

Specification and Verification of Embedded Systems

Embedded software is used in safety critical systems such as cars or aircrafts . Errors in those systems can cause high financial losses, or worse, threaten human lives. With techniques such as testing and simulation a lot of errors are hard to find, as not all corner cases might be taken into account. With formal verification on the other hand, the whole system can be verified. To use formal verification we need a model of the system that has a formal semantics. Timed CSP is a such a formal language to model real-time processes.

The topics are about modeling and to some extent analyzing critical aspects of modern embedded systems with the specification language (Timed) CSP or variants thereof. The focus is on concurrent multicore systems and adaptive systems. We do not consider only specifications but also implementations, e.g., in LLVM.

Example Topics:

  • NEW Abstract representations of processes NEW
    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

Contact: Thomas Göthel, Nils Jähnig

Analysis and Verification of hybrid Simulink-Models

Simulink is a system description language and a tool to model and simulate embedded systems. Systems are created by combining blocks and signals on a graphical user interface. Blocks perform calculations and the results can be transferred to other blocks by signal lines.

It is possible to model systems that contain discrete behavior, which is described by discrete changes in systems values, and continuous behavior, which can be described by differential equations. This enables it to model hybrid systems in Simulink.

The correct behavior of a model is especially important for application in safety critical areas, e.g., in the automotive area or in the medical context. However, with the simulation engine of Simulink, it is not possible to show the absence of faulty behavior. To enable the use of formal methods, to prove the absence of errors, analyses and transformation techniques are used.

The topics in this area are about analyses and transformations of Simulink-models to enable formal verification. With a service-oriented approach, a model is partitioned into sub-models, which perform specialized tasks in a system. With a general representation of such services, it should be enabled to reuse a service in other systems and to reduce the verification effort by using already obtained information.

Current example topics:

  • Integration of Feature Modeling in Simulink
  • Creation of a Simulink Case-Study using Service-Oriented Design

Contact: Timm Liebrenz

    Self adaptive systems with adaptive adaptation logic

    Self-adaptive systems are able to cope with changing environments autonomously. Usually, a predefined adaptation logic (e.g., adaptation rules ) is used to define the adaptation possibilities of a system. These possibilities can be switching between predefined configurations or adjusting system parameters. This static solution allows for a fast reaction to changes but results in problems with environment behaviours that were not anticipated at design-time. In this case, no adaptation rule might be applicable or adaptations might not have the expected effect.
    Another possibility is to dynamically learn the system's adaptation possibilities by using machine learning or model checking techniques. As these techniques have a higher time and memory consumption as static adaptation rules, we examine a combination of both approaches. We propose to continuously evaluate adaptation rules, to disable inappropriate rules and to learn new rules if necessary. This also enables us to cope with dynamic changes of the system topology.

    Example Topics:

    • Correction and learning of system / environment models (only available for candidates with sufficient expertise in model learning)

    Contact: Verena Klös

    Security using Artificial Software Diversity in Safety-Critical Real-Time Systems

    Cyber-Physical Systems (CPS) have an ever increasing impact on our life as more systems are controlled by computers, which are highly interconnected and even connected to the internet. Among these systems are hard real-time systems such as airbag or ABS controllers, where missing a deadline is considered a system failure. If such a functionality is safety-critical, e.g. the ignition of an airbag, the developer is required to provide guarantees on safety and timing properties.

    When safety-critical systems are exposed to potential attackers, assuring safety implies also dealing with security issues. In particular, control-flow attacks are a threat to CPS. Existing countermeasures cannot be applied due to limited resources or limited operating system support.

    The focus of our work is the development of methods that allow applying artificial software diversity, as a proven security measure, to safety-critical real-time systems. Our work involves analyses and manipulations of low-level code representations such as assembler, and different aspects of static worst-case execution time (WCET) analyses.

    Example Topics:

    • developing a load-time diversity approach for real-time OS
    • extending existing WCET cache and branch prediction analyses to support diversity

    Contact:

     

     

    Model based Deployment for Industrial Internet of Things Applications

    With the growing interconnection of embedded systems, e.g. associated with smart factories and Industry 4.0, Industrial Internet of Things (IIoT) applications are gaining in importance. An example use case for such applications in the industry is the interconnection and monitoring of distributed production facilities.

    To systematically develop IIoT applications, there are much less computer-aided development tools available than for conventional applications. Existing approaches in model based development mostly focus on the application's functionality and leave out the fundamental communication setup, the integration of existing components, partly with proprietary protocols, and the deployment of the application.

    Against this background, in cooperation between SESE and an external PhD candidate, who works at HARTING IT Software Development, a framework is being developed to ease the model based development of IIoT applications. The framework is intended to automate the software development lifecycle phases as far as possible.

    Informations derived from the abstract application model are supposed to be used to generate the fundamental IP based communication architecture, preferably automatically. Besides that, the automatic deployment of the whole application should be made possible.

    Example Topics:

    • Evaluation of model based development approaches in the IIoT domain
    • Development of a webbased modelling tool for IIoT applications
    • Development of proxy components for proprietary protocols, like e.g. Modbus or I/O Link
    • Systematic migration from IPv4 to IPv6 for existing IIoT applications
    • Development of IIoT applications as case studies

    Contact: Benjamin Feldner

    Zusatzinformationen / Extras

    Quick Access:

    Schnellnavigation zur Seite über Nummerneingabe

    Auxiliary Functions

    Contact

    Joachim Fellmuth
    +49 (30) 314 - 24789
    Room TEL 1007