Cyber-Physical Systems (CPS) integrate computational processes with physical processes. Different systems are summarised in this term, from cars, trains, and aircrafts to modern smart home systems. These systems must meet requirements of openness, connectivity, increased software-implemented functionality, flexible configurability, dependability, and resilience, all in a cost-effective way, and during all phases of their life-time. The limitations of current CPS design approaches become obvious when trying to fulfil these requirements simultaneously. The central concept to cope with the ever-increasing complexity of CPS, alongside functional decomposition, is the definition of views which enable the specialisation of developer roles. While dealing with component dependencies is well researched, the unsolved scientific challenge of view consistency is the central reason for the above-mentioned trade-offs between configurability, functionality, dependability, and cost-effectiveness.

The aim of this CRC is to develop a general, comprehensive understanding of view consistency and mechanisms to detect and, when possible, automatically or interactively resolve consistency violations between views in CPS design. Therefore, we will investigate how to extend, generalise and transfer work in the area of view consistency in software engineering to systems engineering. The CRC will be formed around the methodological core of a so-called virtual single underlying meta-model that has been investigated by the applicants. We see a window of opportunity as elaborated meta-models of non-software domains are now being standardised. This gives us the chance to research the extension of our software engineering approach to non-software views of CPS.

SFB 1608: CONVIDE – Consistency in the View-Based Development of Cyber-Physical Systems

Pilot Programme Core Informatics (KiKIT) is the incubator of a research project in the Helmholtz Association with the aim of making it permanent from 2026. KiKIT comprises three sub-areas: Algorithm and Software Engineering; Data Science, AI, and Human-Computer Interaction, as well as Hardware and Networks.

Prof. Beckert's group is participating with two projects: Algorithm Refinement and Integration of KeY and KeYmaeraX (https://keymaerax.org) at KiKIT.

KiKIT

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

KASTEL Project

KIT currently offers the possibility to conduct online polls. Thereby, conducting open votes, e.g., within video meetings of committees, is relatively easy. However, secret online votes and elections pose a disproportionately greater challenge – due to the opposing requirements which result from the secrecy of the ballot on the one hand side and the need for traceable correctness and election security on the other hand side.

The goal of this project is the design and the prototypical implementation of an online voting system for end-to-end verifiable, secret elections at KIT. The prototype will be employed for a KIT-wide straw poll. The aim is notably not to change the decision-making power, but to explain complex technical situations. Firstly, there is already a dynamic that evolves towards online elections at universities, presently however generally in the form of black-box systems for which strong security assumptions are made.

Project for E2E Elections at KIT

KeY was successfully used in multiple research projects that were not initiated by the KeY team. While this proves the potential of KeY as a research tool, it has to be said that the majority of these applications were performed in collaboration with members of the KeY core team.

The main goal of this project is to make KeY so usable and robust that it can be successfully applied by computer science researchers outside the KeY team. We provide KeY as a test bed for experiments in the area of formal methods, and as a platform for new approaches and methods for ensuring and analysing the reliability of research software.

This project is funded by the DFG.

Since the beginning of the pandemic, online voting systems have been increasingly discussed and used in secret elections and polls. On the one hand, the question is raised as to the technical and organizational trustworthiness of the systems used (i.e., how the security of these systems is assessed in the course of an evaluation of their properties) and, on the other hand, as to how the voters’ trust in these systems (and ultimately the outcome) is influenced and what role explainability plays in this context (i.e., to what extent voters understand the functionality and/or properties).

The goals of this project are a networking of the two topics Engineering Secure Systems and Knowledge for Action in the Helmholtz program Engineering Digital Futures (within the research field information) as well as an impulse for special research questions in the context of technical-organizational trustworthiness and influences on trust in online voting systems, particularly concerning the role of explainability.

Networking Project for Explainable Online Elections

The aim of the SofDCar project is to increase digital sustainability in the automotive sector. This is achieved by improving rules, processes and infrastructure in the area of software updates and upgrades. The aim is to make the updates more controllable with a strong focus on safety and security. This will make it possible to develop new functions, in and around the vehicle, that can be developed more quickly and safely to the drivers.

SofDCar Project

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

KeY Project

Computational social choice is a rapidly evolving research trend concerned with the design and analysis of methods for collective decision making. It combines methods from computer science with insights from economic theory. COST Action IC1205 on Computational Social Choice is a European research network that has been set up to provide a common platform for research in this field across Europe and beyond.

Within this project, we focus on the specification and verification of voting rules. A voting rule, as a method to combine individual preferences to an aggregated election result, is part of the fundamental democratic principles. It is thus vital that voting rules are working as intended. The goal of this project is to develop formal verification techniques which allow to check properties of voting rules without the huge overhead of user interaction needed in full functional verification. The resulting methodology could then be used in an iterative design and implementation process of new voting rules.

COST Action

The main goal of the project Lehre^Forschung-PLUS is to improve the study conditions and to continuously raise the qualitiy of teaching by an extensive development of the curricula for bachelor and master students.

Our subproject comprises three primary actions, which all aim to implement and strengthen project- and research-oriented, as well as interdisciplinary, teaching in the computer science curricula.

These comprise the further development and improvement of the project- and research-oriented master module "Research Project", the project-oriented bachelor module "Software Engineering Practice", as well as the introduction of the interdisciplinary and research-oriented master profile "Internet and Society" [PDF].

Subproject "Lehre^Forschung-PLUS – Problem-oriented, Research-oriented and Interdisciplinary Teaching in Computer Science"

In order to cope with the challenges from digitization as adults, pupils need a comprehensive basic education in computer science. In the open-source teaching software laboratory, pupils are to gather practical experiences in developing open source software and simultaneously create material for computer science teaching in schools.

OSLSL Project

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.

IMPROVE-APS Project

The goal of this project is to pave the way for specification and formal verification of smart contracts. Building on existing verification tools and technology, we establish a base for describing and proving functional properties of smart contracts. The overall goal is that blockchain/smart-contract technology, with all its advantages, can be confidently employed.

VeriSmart Project

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

Goal of the Software Campus programme is the training of tommorow's managers with excellent IT background. Projects in the scope of the Software Campus programme are supported by scientific and industrial partners.

The project "Formal Information-Flow Analysis of Component-Based Systems" is a project in collaboration with DHL IT-Services in Bonn and aims at performing security analysis of component-based systems during system design.

FIfAKS Project

The main goal of the project "Lehre hoch Forschung" is enhancing study conditions and teaching quality as well as the integration of research topics into early stages of the study programme for bachelor and master students.

Moreover, “Lehre hoch Forschung” is aimed at offering a wide scope of prospective problem-oriented and research-oriented practical courses and projects to students already during their early semesters. The students gain insights into aspects relevant to fundamental and applied research, as well as inter- and trans-disciplinary competences.

Our group is responsible for the establishment and coordination of the master course module "Research Project". This is a project-oriented course in which students learn how to do research projects: from the early stages of writing a project proposal to performing the project tasks and writing publications. The projects are performed on topics within current research projects.

Subproject "Lehre hoch Forschung – Problem-oriented Teaching"

The goal of this project is to leverage advances in deductive program verification to enable regression verification, i.e., proving formally that software remains correct through its evolution, and no new bugs are introduced. We aim to develop a regression verification methodology for a real object-oriented language (Java) that has the reach and power to be applied to real-world software

IMPROVE Project

In diesem Projekt werden Testverfahren und formale Methoden kombiniert um die Zuverlässigkeit von evolvierender Software zu gewährleisten. Mit dem Fokus auf evolvierende Software behandeln wir eine wichtige Phase im Lebenszyklus eines Softwaresystems und heben die inkrementelle Natur von Softwareänderungen hervor.

GIF Project

Goal of the Software Campus programme is the training of tommorow's managers with excellent IT background. Projects in the scope of the Software Campus programme are supported by scientific and industrial partners.

The project "Usability of Software Verification Systems: Evaluation and Improvement (USV)" is a project in collaboration with DATEV eG in Nürnberg and aims at evaluating the usability of software verification systems. Based on the evaluation results mechanisms will be developed to improve the productivity of such systems.

USV Project

COST is the acronym for "European Cooperation in the Field of Scientific and Technical Research".  It is an inter-governmental framework for fostering collaboration between researchers in Europe in a "bottom-up" manner. More information about COST can be found at the official COST website. COST is organized in Actions. The goal of this Action is to co-ordinate the development of verification technology, to achieve reach and power needed to assure reliability of object-oriented programs on industrial scale.

COST Action

The integration of deductive software verification and bounded model checking (BMC) is subject of our current activities and is joint work together with the working group of Dr. C. Sinz.

Proving software correct using deductive verification methods needs — in addition to the requirement specification — a variety of interactions by the user of the tool (e.g., giving loop invariants or specification of auxiliary functions). In contrast, BMC to a large extent doesn't rely on user support in proofs. On the other hand, deductive program verification features a higher precision and a more expressive specification language compared to BMC.

A first goal of the work in this project to combine the strengths of both methods is to use BMC to improve interaction of the user with the deductive verification tool. By linking a BMC-tool to a deductive verification framework, parts of the specification of a program can already be checked even before starting with the whole deductive proof.

The correct functionality of systems, as used in e.g. automotive or in the area of safety engineering, is checked using formal, mathematical methods.

Scenarios

• automotive applications
• avionic applications
• operating systems and hypervisors

Formal correctness proof of an embedded operating system kernel

The main focus of the investigations of our research group is on the specification and verification of a microkernel with partitioning features which is used in industrial avionic applications. For this we employ the verification tool VCC developed by Microsoft Research,  to formally verify functional properties of the implementation of the microkernel PikeOS from SYSGO AG.

Verisoft Project