Research
The overarching question that drives our work is: How can we ensure that a software system meets our requirements in the intended operation environment? Answers to this question usually include four working directions:
- modeling assumptions on the intended operation environment,
- formalizing our expectations into testable requirements,
- checking requirements on a system under the made assumptions, and
- supporting the corresponding tasks with tools, processes, and standards.
Safe Autonomous Systems
Safety of autonomous vehicles is an open challenge. In recent years, scenario-based testing has been researched as an assurance method. In scenario-based testing, the assurance effort is decomposed into different driving tasks. To understand the feasibility of this strategy, it is important to better understand and formalise traffic and traffic rules (i.e., functional requirements on autonomous vehicles).
To this end, we have contributed to a method for classifying driving manevuers that is cited in the ISO 21448 SOTIF standard (Safety of the intended functionality). We have proposed a process for identifying triggering conditions, i.e., environmental factors that trigger functional insufficiencies in autonomous driving software. We currently work on a formal language for specifying the operational design domain (ODD) of autonomous vehicles.
Domain-Specific Modeling Languages
Only formalized requirements can be checked automatically. Unfortunately, engineers are usually not well-trained in formal logic and, especially for cyber- physical systems, formal requirements become complex quickly. We are convinced that we need to enable engineers to write precise requirements in a language they understand. W
We have several past and ongoing projects in which we develop domain-specific languages. In the BMBF funded QuARUm project, e.g., we develop domain-specific languages in which geologists from University of Bremen can express their data analysis pipelines and data quality requirements.
Formal Methods for the Analysis of Software
Since the systems that we build are highly complex and modern execution environments have rich features, the behavior of systems in many cases emerges only at runtime. To analyse emergent behavior, we develop dynamic methods that integrate static and symbolic techniques for stronger guarantees.
We develop a modular dynamic analysis framework (incl. symbolic execution and dynamic taint analysis) that can analyze Java, Kotlin, and Scala programs. Prototypical extensions for C and JavaScript have been developed in thesis projects. Our verification tools compete successfully in SV-COMP, the software verification competition.
Automata Learning
In many instances, it is not possible to manually model the environment or to obtain a model of black-box system. It is, however, possible to either learn models of the environment from observations or to replace the environment of a component by an active learner who is allowed to take all the actions of the environment to learn a behavioral model of the component from tests.
We develop active and passive automata learning algorithms for different types of extended finite state machines. Most of these algorithms are implemented in these tools:
Sovereign Sharing of Data
IoT Devices and 5G technology will make it possible to put computing power and sensory equipment everywhere and connect decentralized computing power in huge distributed, heterogeneous architectures, spanning IoT devices, edge-resources, and cloud platforms. The main novel capabilities of such cyber-physical systems are (a) the distributed observation, analysis, and processing of data, and (b) decentralized control of the physical world.
We need organizational, constructive, and analytical approaches for making distributed data-intensive systems reliable and secure. One important aspect to consider is the data-sovereignty of users of these systems. We collaborate with Fraunhofer ISST on the technical foundations of sovereign data sharing. This includes, e.g., domain-specific languages for modeling usage policies and formal analyses for guaranteeing sovereignity.
Web-Application Security
Containerisation, inversion of control, dependency injection, aspect oriented programming, and mocking make it hard to precisely analyse the security of modern Web applications and app backends.
We work on the analysis of Web application security with the program analysis tools we develop — integrating taint and information flow security analysis with dynamic symbolic execution and other techniques for discovering execution paths.