Property-Based End-to-End Analysis of Cause-Effect Chains (PEACH)

• Applicant: Dr. Mario Günzel
• Subject Area: Computer Architecture, Embedded and Massively Parallel Systems
• Term: since 2025
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 569077889

While in general computing systems the correctness depends only on the logical result (i.e., the correct output is computed for any input), for some systems the correctness also depends on the physical time when the result is provided. Such real-time systems can be found in several applications like smart homes, medical technology, traffic management, airplanes, cars, logistics and manufacturing. In many real-time systems, the interplay of tasks (i.e., the transfer of data between them) is a critical aspect. For example, a typical (simplified) automatic braking system can be modeled as a sequence of tasks: First, a camera image is taken, then image recognition marks objects (such as pedestrians, walls, and other vehicles) in the image, and eventually, danger analysis determines whether the car must be stopped to avoid a harmful situation. This sequence of tasks is called a cause-effect chain, and an end-to-end analysis determines the time required for the data to be processed by each task and passed along the chain. Existing analyses are often ad-hoc and rely on restrictive assumptions, i.e., for the analysis of deterministic end-to-end latency usually a specific model for communication and task triggering mechanism is assumed, and the analysis of probabilistic end-to-end latency relies on strict independence assumptions, which limits their generalizability and applicability. To address this gap, this project will establish a property-based perspective on the analysis of end-to-end latency of cause-effect chains. Specifically, it will develop analytical results based on system properties rather than specific models, to build more general and modulable solutions. To that end, this project focuses on three main objectives. The first objective is the development of monotonicity and dominance relations for end-to-end latency of cause-effect chains, to enrich the repertoire of fundamental properties (i.e., compositional property and the equivalence of metrics). Monotonicity and dominance are central mathematical concepts that enable the transfer of analytical results to related scenarios, and therefore they are essential for developing more general and modulable solutions. The second objective is the property-based analysis of probabilistic end-to-end latency, tolerating occasional violations of real-time requirements. While such probabilistic guarantees are highly relevant for many industrial applications, existing approaches are limited, with only a handful of solutions that rely on strong independence assumptions. Applying a property-based perspective, these limitations will be overcome, leading to more versatile and practical results. The third objective is to collect and release analyses as part of an open-source toolbox, to ensure the accessibility of the results developed throughout this project and allow comparison with other approaches.

• DFG Programme: Research Grants