KiKIT

In the information age, computers are a key driver in all areas of research, technology, business, and society. Therefore, high-quality software, hardware, and AI models are necessary to maintain digital sovereignty and need provisional research. Through the Pilot Program Kerninformatik am KIT (KiKIT), the research on core informatics is to become a focus of Helmholtz research. KiKIT focuses on the research of novel general methods in the fields of algorithm and software engineering, data analysis, and machine learning as well as hardware and network systems. Moreover, KiKIT pursues the goal of providing stable research tools (research software, AI models, etc.) to accelerate other research activities within Helmholtz as well as to support innovation in industry.

SFB 1608 Convide

At the Collaborative Research Center 1608 “Consistency in the View-Based Development of Cyber-Physical Systems”, researchers with a background in computer science, mechanical engineering, and electrical engineering join forces to create solutions designed to tackle the immense complexity of current and future cyber-physical systems (CPS). We are developing a methodology for CPS across various design spaces of different engineering disciplines ensuring short release cycles, high dependability, and high configurability. Following our vision will enable us to formulate a new role of software engineering as an exporter of methods within systems engineering.

SofDCar

All project partners of the SofDCar Alliance are focussing their research on the challenges of future E/E & SW architecture in vehicles.

Each vehicle is seen as one piece in a network of all vehicles and the infrastructure. Its integration will be enabled via “data loops” and new-type “digital twins”, thereby paving the path to digital sustainability (of today’s and tomorrow’s vehicle generations) and enabling efficient data structures and innovative use cases throughout the whole vehicle lifetime (Re-Deployment).

This project is part of a government-sponsored research program. It is sponsored by the German Ministry of Business Affairs and Climate Control (BMWK).

KeY

The KeY System is a formal software development tool that aims to integrate design, implementation, formal specification, and formal verification of object-oriented software as seamlessly as possible. At the core of the system is a novel theorem prover for the first-order Dynamic Logic for Java with a user-friendly graphical interface. The project was started in November 1998 at the University of Karlsruhe. It is now a joint project of KIT, Chalmers University of Technology, Gothenburg, and TU Darmstadt. The KeY tool is available for download.

Change APS

Depending on the industrial sector, an automated Production Systems (aPS, i.e., machines and plants) are subject to strict regulations, which affect changes made to an aPS during or after commissioning and start-up. In sectors affected by legal regulations, e.g., the medical field, changes must be documented in standardized change tracking workflows to prevent undesired side effects. Certain change types or scopes even require a complex recertification process. Instead of going through test executions again, regression verification with appropriate specifications would support shortening and partially automating the revalidation processes and provide documentation to ensure the software’s behavior is as intended.

KASTEL

The main topics intelligent infrastructure, cloud computing and public security challenge the IT security of the future. In addition to the classical term of security one has to deal with threats from the inside as well. It is not enough anymore only to look at security issues of system components. We have to focus on transdisciplinary methods. The Kompetenzzentrum für Angewandte Sicherheits-TEchnoLogie (KASTEL) is a research center for cyber security and combine several areas of IT security and their users.

IMPROVE APS

The vision for this project is to advance technology such that regression verification methods are available that will be routinely used for ensuring correctness in the evolution processes for long-living reliable systems requiring frequent re-validation. The goal of regression verification is to formally prove that software remains correct through its evolution, changes have the desired effect, and no new bugs are introduced. Regression verification avoids the main bottleneck for the routine practical use of formal verification, namely the need to write full functional specifications (which is a huge effort). Also, given two program versions or variants that are both complex but similar to each other, the effort for verifying the relation between them mainly depends on the difference between the programs and not on their overall size and complexity.

Program-level Specification and Deductive Verification of Security Properties

Reliably Secure Software Systems – RS³ In recent years tremendous progress has been achieved in formal verification of functional properties of computer programs. At the same time seminal papers have been published showing that it is in principle possible to formulate information-flow problems as proof obligations in program logics. The overall goal of the project is to leverage these advances together with our own experience in formal methods for functional properties in order to specify and verify security properties. DeduSec Project