Tradeoffs in Reactive Systems Design

Today, most complex reactive systems, and especially autonomous systems, are composed of multiple subsystems such as controllers, schedulers, machine learning (ML) components, and security systems. These subsystems are designed independently and are aimed to work to perfection. But in reality they do not work perfectly and the imperfection is assumed to be small enough that it may be ignored. We argue that design approaches should make the imperfections in these components first class citizens, formalize specifying imperfections, and allow tradeoffs in the design play a more prominent role.

Towards this, we first define a flexible notion of system-level safety to admit imperfect behaviors. We then compute which component behaviors would ensure such a notion system safety. This allows more component behaviors compared to those that would be admitted if the component was to be designed to perfection. These additional behaviors allow more efficient component implementations. Further, they allow exploration of tradeoffs where the deficiency of one component may be compensated by another component, while satisfying the notion of system-level safety and the flexibility it allows. To arrive at a general notion of imperfection, we consider the dynamics of closed-loop control systems. First, we determine the trajectory followed by such systems in their state space, when all the system components behave perfectly, e.g., when all the elements of the system state may be estimated exactly, all machine learning components in the system always return accurate inferences, and the deadlines of all software/control tasks are always met. For any given initial condition, such a system trajectory represents the ideal behavior of the system, which might not be practically realizable. To allow imperfect system behaviors, we consider a safety pipe around this ideal trajectory. Any system trajectory that lies within this safety pipe is considered to be an acceptable or safe behavior of the system [4].

It is, however, non-trivial to estimate component behaviors from such specifications of safety pipes that capture system-level behaviors. In this talk we illustrated how this may be done for the specific case of imperfect timing behaviors. In particular, we asked: Given a safety pipe specifying allowed system behaviors, what are feasible timing behaviors that a control task may experience? Our procedure to answer this question involves the following two steps: (1) Guess a regular language $ℒ$ of timing behaviors that a control task may experience [1]. Such a language is a set of strings over the alphabet $\mathrm{\Sigma }=\{0,1\}$. Here, $0$ represents the case where the control task in question misses its deadline at the specified sampling period, i.e., the control input is not available at the time of actuation and an old control input is used. On the other hand, $1$ denotes the case that the control task successfully completes its execution before the predetermined time of actuation. Hence, a string $101010\mathrm{\dots }$ denotes that the case where every alternate execution of the control task misses its deadline. Equivalently, it also denotes the case where the control task is purposefully not scheduled in every alternate sampling period to save computation bandwidth.

In the next step: (2) We use approximate reachability analysis over a bounded time horizon to check whether all the trajectories of the given closed loop system stay within the specified safety pipe, when the control task is subjected to any timing behavior that belongs to the language $ℒ$. Here, we use approximate reachability to contain the state-space explosion that would otherwise happen. If the language $ℒ$ of timing behaviors result in safe closed-loop behaviors (i.e., all the closed-loop trajectories are within the safety pipe) then we add $ℒ$ to the set of safe languages, viz., ${ℒ}_{safe}={ℒ}_{safe}\cup ℒ$, where ${ℒ}_{safe}$ was initially empty. By iteratively following this procedure, we create a set of timing behaviors ${ℒ}_{safe}$ that results in safe closed-loop system behaviors. Now, since the union of regular languages is regular, ${ℒ}_{safe}$ may be represented as a finite state automata. We can use this procedure to synthesize safe schedules for a set of control tasks. For this, we rely on automata-theoretic techniques [5, 9] to combine the ${ℒ}_{safe}$s of all the controllers to synthesize schedules where the tasks of each controller is not always scheduled for execution (i.e., occasionally misses its deadline), but the safety of all the closed-loop systems is guaranteed [10]. Such schedules account for the dynamics of the closed-loop system [2, 3, 6] and cannot be reproduced by standard scheduling policies like fixed priority or earliest deadline first (EDF) [7]. This approach of using a flexible notion of system safety to allow multiple (imperfect) component behaviors allows the exploration of different tradeoffs between the performance of different system components. For example, the work in [11] uses the size of the reachable set as a measure of safety and shows how the size of a neural network – and therefore its inference quality – for state estimation in a closed-loop control system may be traded off with the magnitude of the control input. This is used to partition a deep neural network (DNN) between edge and cloud resources. A similar approach was also used [8] to purposefully choose DNNs with less than optimal size and inference accuracy, to fit multiple DNNs on the same shared graphics processing unit (GPU), while ensuring that the dynamics of the closed-loop systems using these DNN inferences remain safe.

While a safety pipe around an ideal system trajectory, or the size of the reachable set, are two different notions of system safety, there are many other possibilities. For example, not all trajectories within a safety pipe might be permissible. Most work on formal methods till date have focused on specifying perfect or ideal system behaviors (e.g., all deadlines are met). Specifying what kind of imperfect behaviors might be acceptable requires domain knowledge, and those with such knowledge are usually not sufficiently conversant with formal methods to be able to write formal specifications. Hence, new avenues for involving domain experts – who are not specialists in formal methods – to write formal specifications, perhaps using tools from machine learning will be needed.

Security and privacy are growing concerns across all forms of digital systems, including Cyber-Physical Systems (CPS). Embedding intelligence in such systems are done to enhance performance and autonomy. Such an inclusion compromises security, which is often fixed as an afterthought. The talk highlights several instances across the stack of digital systems, from machine learning, general purpose processors to hardened cryptographic implementations, which showcase that security and efficiency present contrasting choices for a system designer. This situation is exacerbated for autonomy, where Artificial Intelligence (AI) is invoked. Lack of explanation in many AI systems directly falls into the hands of a malicious actor, who can compromise the system in many subtle ways.

We present a process for the Verification of neural networks using formal methods, developed to support the needs of Collins engineers working on neural networks for aircraft. The process focuses on low-complexity neural networks (having hundreds or thousands of learnable parameters) with simple input domains (less than 10 input features). It is especially applicable when the neural network is used to approximate a given target function (such as a complex optimization or large look-up table) at a lower computational cost. It compares the behavior of the neural network to the target function by exhaustively verifying the entire input space. Such an exhaustive verification, made possible by using formal methods, analyzes how the neural network would respond not only on the training or test dataset but also to any unseen data in its input range. We anticipate that this approach will be useful for high-criticality neural network-based components (DAL-C and above). It can be used as a means of compliance with certification objectives e.g., stability analysis and generalization capability assessment as defined by the European Union Aviation Safety Agency (EASA). The process is illustrated through a Collins use case, namely the Recommended Cruise Level (RCL) function, which can be used to provide pilots with a suggested altitude to reduce the operational cost of the flight. The process is used to verify a neural network implementation of the RCL, that significantly reduces the computational cost and memory footprint of a traditional implementation.

Tradeoffs represent choices between multiple objectives that are determined by choices between different configurations. This presentation introduces a mathematical framework, a component model and a domain-specific language. The mathematical framework captures the essential operations and requirements to support compositional computation of Pareto optimal configurations of a system from descriptions of the (optimal) configurations of components. It defines a number of relations on configurations, the sets of possible configurations of components or systems to characterize which ones are considered better, worse, or equivalent. The framework provides insight in requirements on the models and operations to work effectively, preserve optimality, etcetera. We further introduce a component model for Quality and Resource Management that builds on Pareto Algebra. It aims to describe application and platform components in a virtualized platform setting. Components are described in terms of input and out qualities, their required and provided budgets, their optimization objectives and the parameters used to configure the component. The resulting system semantics is a set of (Pareto optimal) configurations of the overall system. This set can be implicitly captured as a set of equations in terms of the combined system parameters. We have defined a Domain-Specific Language, called QRML, to specify such component models generated different types of visualization and generate the set of constraints to be checked for satisfiability, or for optimization, by a constraint solver, such as the Z3 SMT solver. The tools are available through the web page https://www.qrml.org.

Many computing systems are constrained by a fixed amount of available shared memory. Modeling applications with task graphs makes it possible to analyze and optimize their memory usage. The NP-complete problem studied here is finding a parallel schedule of a given task graph that minimizes its memory peak.

Our first contribution is an algorithm that finds optimal sequential schedules for a dataflow task graph. This algorithm is based on graph transformation rules. On a large class of graphs, it is able to compress the graph into a single node which contains a sequential schedule optimal w.r.t. the memory peak. The approach also applies to SDF graphs after converting them into task graphs. However, since that conversion may produce very large graphs, we also propose a new suboptimal method, similar to Partial Expansion Graphs, to reduce the problem size. We evaluate our approach on classic benchmarks, on which we always outperform the state-of-the-art.

From this optimal sequential schedule, our second contribution is a dynamic parallel schedule, which consists of a ready list scheduling that we adapt to take into account memory requirements. Our approach always produces a parallel schedule that meets the constraints and enjoys very good speedups. It can also be applied to less harsh memory constraints, leading to more substantial speedups. We compare with alternative approaches on multiple applications expressed as task graphs (scientific workflows, signal processing filters). When memory constraints are close to their minimum, our approach always succeeds in finding a parallel schedule meeting the given constraints, whereas the other approaches mostly fail. When memory constraints are significantly higher, our results are comparable to others for speedup. Furthermore, our approach is faster and can deal with very large task graphs (up to 50,000 nodes) using a naive Python implementation.

Shared-memory systems are a reality of today’s hardware, and current trends are to increase their scale and complexity, with heterogeneous shared-memory architectures and hierarchical systems with protocols like CXL. These systems, however, have complex behaviors that trade consistency with latency, through out-of-order execution and weak guarantees in the protocols, resulting in weak memory consistency models, i.e. models weaker than sequential consistency. In this talk, I present some of the architectural guarantees, and open questions in this context, which give us primitives to express and control tradeoffs in consistency and latency. I argue we should build higher-level abstractions on top of these primitives to reason about these tradeoffs at a higher level of abstraction in the design process, e.g. programming languages or runtime systems.

In the avionics domain, “ultra-reliability” refers to the practice of ensuring quantifiably negligible residual failure rates in the presence of transient and permanent hardware faults. In this talk, I discuss the need for new mechanisms that can help us make contemporary and next-generation CPS, which use inexpensive, relatively unreliable off-the-shelf components, more reliable and, if possible, ultra-reliable (as airplanes). I will frame the discussion around the problem of Byzantine fault tolerance (BFT). Specifically, I will briefly present our RTSS 2022 work, where we proposed a novel BFT timed key-value store, called Achal, designed specifically for Ethernet-based distributed real-time control applications. I will then describe our current work on understanding two key limitations of Achal-like systems. First, can they be seamlessly ported to real, complex CPS applications? Second, can precision time synchronization be considered a reliable primitive? Finally, I wrap up with my key takeaway, that we must focus on systems / middleware / tools that make it easier to engineer reliable systems, as opposed to designing new fault-tolerance protocols from scratch.

Engineering Reactive Systems primarily involves evaluating the accuracy of computations, as well as the system’s quality attributes (such as safety, security), or its functions or data (such as availability, consistency). This list is not exhaustive, and neither is this mapping. These properties can be assessed by testing the final system. A more timely and cost-effective approach is to rely on models and verification and validation (V&V) techniques such as simulation or model checking. Evaluating these quality attributes necessitates the construction of an additional system: a model and a demonstration that the model is sufficiently accurate to both represent the system and support a verification objective.

In this presentation, I propose some considerations in the scope of Dagstuhl Seminar 25091. Firstly, when considering a model as a system, it is crucial to define its requirements. The term “capturing a system behavior” is too ambiguous. A model should support an engineering goal, such as evaluating a system attribute. Therefore, the selection of a modeling language, the creation of the model, and the property to be evaluated cannot be separated. It is essential to ensure that the evaluation of an attribute or a tradeoff analysis among multiple attributes can be initially expressed in a model and then analyzed by some techniques. This can only be achieved if the modeling language is sound, the model captures a domain taxonomy, and, of course, it is correct.

Before aircrafts are approved to carry passengers, the industry has to provide evidence to the aviation authorities of the safety and conformity of their products. This approval is called “certification”. And is achieved by conducting a very thoroughly documented process of addressing every foreseeable failure with safety impact. This process is particularly stringent with failures of catastrophic or hazardous consequences. This talk briefly describes this process for avionic equipment (computers). For functions with minor safety impact, COTS or COTS-like “Design Assurance Level” (DAL) could be considered. At such a level, low energy (edge) AI technology could already be considered. But for higher Assurance Level, achieving this objective may require a thorough understanding of the technology, exhaustive (including formal) design checking, use of diverse strategies for error detection, and resource redundancy. The purpose of this talk is to give academics with intent to assist industry by providing tools, methods, languages and IP in general, an understanding of the level and nature of information (documentation and support) the industry needs to adopt their proposals.

This talk will introduce the Distributed Rhythm Generator, a distributed real-time program written in Lingua Franca. Distributed real-time systems are intriguingly challenging systems, as they must balance two opposing requirements. First, they must often only actuate based on a consistent view of the shared variables of the overall system, and second, they must actuate in a timely manner. Without time-predictable networks, reconciling these requirements might not be possible and a tradeoff must be made. We will show how the reactor-oriented programming paradigm introduced by Lingua Franca, enables an elegant specification of such consistency-available tradeoffs.

The current trends in hardware design aim at improving the average performance. Together with the increase in software complexity, this trajectory runs contrary to time-predictability, especially when designing safety-critical and real-time systems, as timing requirements need to be guaranteed a priori. Literature is rich with valuable attempts to define and measure time-predictability. Still, a quantitative approach that covers all the different features at the different abstraction levels is missing. This talk suggests the design of a concept map for time-predictability levels. It is based on results from different research papers and is meant to be extensible to accommodate future inventions. It is also derived from expert knowledge in the different fields. The concept map, when combined with multi-criteria decision techniques, can formalize the choice among two or more designs. The techniques to be used are the Brown-Gibson Model and the Analytic Hierarchy Process. The former has the advantage of combining objective and subjective factors that immediately derive from the concept map. Because weighted scoring is required in this method, we use the Analytic Hierarchy Process to weigh the features among each other. A challenge though is about the support of multi-processor systems with different architectures. In addition, the use of the worst-case performance can be decided to be used either as a validation tool or to perform fusion of the results.

Together, a digital twin and its physical counterpart can be seen as a self-adaptive system: the digital twin monitors the physical system, updates its own internal model of the physical system, and adjusts the physical system by means of controllers in order to maintain given requirements. As the physical system shifts between different stages in its lifecycle, these requirements, as well as the associated analyzers and controllers, may need to change. The exact triggers for such shifts in a physical system are often hard to predict, as they may be difficult to describe or even unknown; however, they can generally be observed once they have occurred, in terms of changes in the system behavior. This talk presents an automated method for self-adaptation in digital twins to address shifts between lifecycle stages in a physical system, based on recent work [1]. Our method is based on declarative descriptions of lifecycle stages for different physical assets and their associated digital twin components. Declarative lifecycle management provides a high-level, flexible method for self-adaptation of the digital twin to reflect disruptive shifts between stages in a physical system.

In this framing discussion, I explore the fundamental tradeoffs between security and accessibility in designing reactive and cyber-physical systems (CPS). This discussion examines how secure access mechanisms – such as authentication, encryption, detection, and mitigation – must balance with the need for accessibility. Through real-world examples and case studies, I highlight the challenges of designing secure reactive systems and CPS while managing the tradeoffs between security and accessibility, considering threat models, costs, and security requirements of the target systems. Various design decisions, including connectivity, encryption strategies, and the choice between prevention and detection of cyber threats, are analyzed in the context of modern threat models. This framing discussion also presents a methodology for enforcing security without sacrificing essential accessibility, ensuring the domain-specific reactive systems and CPS are secure and protected yet accessible.

Distributed software systems often require consistent shared information. For example, connected vehicles require agreement on access to an intersection before entering the intersection. It is far from trivial, however, how to achieve consistency, or even how to define it rigorously enough to know when it has been achieved. In this talk, I will show how strong and weak forms of consistency can be defined, how software infrastructure can provide reasonable guarantees and efficient implementations, and what are the fundamental costs of achieving consistency that no software system can avoid. Specifically, I will outline the CAL theorem, which quantifies consistency, availability, and latency, and gives an algebraic relation that shows that as latency increases, either availability or consistency or both must decrease. I will describe a coordination language called Lingua Franca that enables programmers to explicitly work with the tradeoffs between these three quantities.

In 2000, Eric Brewer (UC Berkeley) famously stated the CAP theorem during the PODC keynote. However, the tradeoffs mentioned in the theorem was not formally specified. Lee et al. [1] later proposed the CAL theorem, which establishes a mathematical relationship among the three properties: Consistency, Availability, and Latency (extending Partitioning in the CAP theorem). In this talk, we present a work-in-progress formalism based on the CAL theorem, which aims to 1) be easily applicable to programming frameworks, and 2) capture the behavior of a reactive system over time. We demonstrate the formalism on a simple stock exchange application written in the Lingua Franca (LF) coordination language. We derive timing constraints from the semantics of the LF language and the application, formulating a system of equations calculating earliest firing times of reactions from previous firing times and asynchronous inputs. We represent the system of equations into a linear difference equation using the max-plus algebra and show that the eigenvalue of a coefficient matrix represents the threshold of the system’s responsiveness.

Real-time systems rely on tasks with well-defined worst-case execution times (WCET) to ensure predictable behavior. To facilitate accurate WCET estimation, some researchers advocate for processor architectures that simplify timing analysis, known as precision-timed or time-predictable architectures. However, the precise definition and quantification of time predictability remain open questions. This talk examines the concept of time predictability and the challenges in measuring it. Instead of focusing solely on architectural properties, we argue that worst-case performance should be evaluated as a combined property of the processor, compiler, and WCET analysis tool. To enable systematic evaluation, we propose to standardize on a benchmark suite for assessing time-predictable processors, compilers, and WCET analysis tools. We define worst-case performance as the geometric mean of WCET bounds across this benchmark set.

The purpose of the talks was to present some of the results reached for introducing ML (Machine Learning) algorithms in Airborne systems. First a brief introduction on certification and on current drafted standards for ML was done. Indeed, EASA is writing roadmaps and preliminary guidance. SAE/EUROCAE working group is in parallel writing a future ED/ARP document. The presentation then has dug to two use cases. The first was the simplest: how to replace a set of LUT (look-up tables) – here for the avoidance collision system ACAS Xu – with neural networks while preserving the intended function. For that, formal verification was successfully applied. These kinds of surrogate models to compress existing code is a way forward. The seconds case is exploratory: vision-based perception algorithm to detect runway during an aircraft landing. Again formal verification was successfully applied to check robustness against some foreseeable perturbations. These preliminary results open the path for certification.

Timing attacks exploit variations in execution time to leak sensitive information. Hardware-software leakage contracts are a new security abstraction that augments the instruction-set-architecture (ISA) to capture microarchitectural leakage at software level. In recent work we have shown how to verify that open-source RISC-V processors satisfy particular contracts and how to synthesize precise leakage contracts for a given processor. In this talk, I motivate and introduce leakage contracts and I discuss two equivalent notions of contract satisfaction that suggest synergies between research on timing predictability and microarchitectural security.

Reactive systems have a rich history of rigorous modeling and verification techniques. As modern verification efforts become more ambitious, they require the composition of a growing number of techniques. This composition necessitates interfacing between different formalisms and tools, which can lead to error-prone discontinuities in the verification pipeline. While there exist systems for coherently verifying reactive systems, they are limited in expressivity. Interactive theorem provers (ITPs) provide a means of verification with virtually unbounded expressiveness, but do not natively capture the semantics of notions like concurrency and mutability. We discuss the problems encountered when attempting gap-free verification of reactive systems in ITPs.

Synchronous languages build on an abstraction from physical execution time by dividing the execution into logical ticks. However, they say little about when to execute the ticks and traditionally lack built-in support for physical time. This makes it rather cumbersome to express things like time-outs or periodic executions. We present Timed SCCharts that use a timed automata formalism and combine it with the concept of dynamic ticks. This enables specifying time-dependent behavior while addressing tradeoffs in timing in the face of imperfections of execution with physical time.

One application area we plan to explore is the railway domain, as part of the REAKT initiative. This initiative aims to revitalize rural rail lines, using the line Bad Malente – Lütjenburg as real world laboratory. As an aside, in Germany alone, about 5000 km of rural train lines have been put out of service since the 1990s. This corresponds to about 30% of the total network, and it directly affects more than 3 million citizens.

As the automotive research and development field approaches automated driving levels SAE L4 and L5, the introduction of the requirement for the driving function to continue operation when an abnormal system behavior occurs becomes crucial. Highly automated and autonomous systems cannot use a human driver as the fallback decision-maker and actuator, and, in order to be safe, they must possess the ability to function until the vehicle reaches a safe state. This talk briefly introduces the concept behind fail-operational systems. First, we introduce the advances of such systems when compared to the fail-safe implementations. We further provide an example of a fail-operational architecture. In the last part of the talk, we discuss the challenges the automotive industry faces when developing fail-operational driving functionality. They include the assurance of independent redundancy, tradeoffs in performance and safety, as well as the development costs. Finally, we address the approaches intended to handle those issues, such as redundant system design, the introduction of monitoring safety components, and the handling of the high safety integrity levels.

Conventional wisdom suggests that the benefits of functional programming no longer apply in the presence of even a small amount of imperative code, as if the addition of imperative code effectively subtracts. And yet, as we show in this talk, combining functional programming with the special imperative language Esterel provides a multiplicative improvement to the benefits of functional programming.

To illustrate these benefits, the bulk of this talk consists of an in-depth exploration of HipHop code (a mashup of JavaScript and Esterel) that implements a Sudoku solver, showing how it is possible to write code that is as easy to understand as if it were written in a pure functional programming style, even though it uses multiple threads, mutable state, thread preemption, and even thread abortion. Even better, concurrent composition and task canceling provide significant program structuring benefits that allow a clean decomposition and task separation in the solver.

A potential problem that may arise in the domain of distributed control systems is the existence of more than one primary controller in redundancy plans which may lead to inconsistency. We worked on an algorithm called NRP FD (Network Reference Point Failure Detection), proposed by industry, to solve this issue by prioritizing consistency over availability. I explain how by using modeling and formal verification, we discovered an issue in NRP FD where we may have two primary controllers at the same time. We then provide a solution to mitigate the identified issue, thereby enhancing the robustness and reliability of such systems. In the same context, I will also show how we used model checking for making informed decisions in designing test cases for fault-tolerant systems. I will add a discussion on how this approach may be generalized in different contexts.

This talk explores the timing and accuracy tradeoffs from application problems in transportation cyber-physical systems. The talk demonstrates previous proof of dampening traffic waves in closed road scenarios, and evidence that existing adaptive cruise controllers amplify (rather than reduce) traffic waves. To address these issues, the work discusses the use of hierarchical high-latency and low-latency controllers, which were shown to be successful. These approaches utilize shared information of the road network that may be gathered over recent minutes, for the purposes of reducing stop and go traffic waves. Given the dynamics of freeway traffic, where speeds of up to 35 m/s regularly encounter stop and go waves traveling at -4 m/s (i.e., against the flow), the lookahead of the on-vehicle sensors is insufficient to dampen these waves, and external information is needed. Using only local sensors it is possible to avoid collisions, but it is not trivial to also dampen the traffic waves. Thus it is important to understand how to share data on downstream state information, with timing information to help understand how to interpret those data. The talk transitions to discussion on how to design and utilize safety envelope controllers for future experiments, in which AI or other untrusted controllers are fielded in open road scenarios. While these controllers can be theoretically shown to be safe, the theory requires information from vehicle sensors (such as derivatives of velocity or acceleration) which are difficult to obtain, and for which filtering delays the availability of the data – requiring an additional following gap for safety that may reduce the effectiveness of the approach. The conclusion calls for continued exploration in determining the accuracy of these distributed systems, which are loosely coordinated, when it is impossible to recreate the situations in which they were fielded. Further, it calls for understanding how one can safely field AI-based controllers to gather field training data, when there may be significant limitations in understanding how safe the safety envelopes are for general use.

This work is supported by the US National Science Foundation, and the US Department of Energy.

This talk surveys the research landscape surrounding the fundamental tradeoff between timeliness and accuracy in complex systems. It explores formal and informal approaches to managing this tradeoff from multiple perspectives, including neuroscience and psychology, scheduling theory, algorithm design, system architecture, and multi-agent systems. Connecting research from the late 1980s to cutting-edge developments, the talk examines how current abstractions, particularly those related to accuracy (e.g., algorithmic precision) and timeliness (e.g., system timing requirements), hold up in the face of increasing system complexity. A core question explored is whether these abstractions remain adequate, or if we need fundamentally new approaches beyond reliance on testing and benchmarking in real-world environments, to effectively address the timeliness-accuracy tradeoff across algorithms, runtime systems (including hardware), and requirements. Finally, the talk identifies key open research questions in this area.

In resource-constrained environments like rural Ghana, designing reactive systems for critical applications, such as smart agriculture and detecting pollutants from illegal mining activities, demands confronting unavoidable tradeoffs. These systems must balance competing priorities shaped by limited energy, connectivity, and financial resources. This has forced researchers to examine how fundamental engineering limits force compromises between accuracy, timeliness, security, and scalability. Researchers cannot eliminate compromises but formalize them, embedding transparency into system architecture. By doing so, they create solutions that are survivable, equitable, and aligned with the pragmatic realities of communities like Ghana’s – where “good enough” is not a concession but a necessity. My presentation at Dagstuhl Seminar 25091 illustrates a broader truth that in resource-constrained environments, tradeoffs are not design failures but fundamental constraints.

Selecting software components to reuse as a means to reduce development time and costs can be challenging, especially when multiple components provide the same functionality but offer different non-functional properties, e.g., numerical accuracy, memory footprint, power rating, timeliness, robustness, security, or financial cost. In this talk, we seek to model the benefit that a system gains from a component’s non-functional properties using so-called “Property-Utility Functions” (PUFs) as a means to formally analyse tradeoffs in component selection. We will discuss how a PUF can model the incremental benefit (utility) that a system would receive for each additional unit of resource that a component consumes. We will explore open challenges in how the utility of a datum or event is transformed by the PUFs of the components they flow through, how to tradeoff one component for another based on their qualities, how to compose and decompose PUFs for bottom-up and top-down system design, and how to diagnose violations in expected utilities.

The work group on “Benchmarks for Real-Time Systems” discussed the shortcomings of existing benchmark suites like TACLeBench and explored possible directions for developing more representative and useful benchmarks. TACLeBench was criticized for being largely composed of small, non-real-time benchmarks, lacking multi-threaded code, and using only fixed inputs. Furthermore, it does not offer standardized licensing, nor does it provide clear guidance on the context in which benchmarks should be executed or evaluated. These limitations make it ill-suited for evaluating modern real-time systems, which are increasingly complex and heterogeneous.

Participants noted that existing real-time benchmarks are used for a range of evaluation purposes – such as analyzing the worst-caes performance and/or predictability of microarchitectures, assessing WCET (Worst-Case Execution Time) analysis tools, and evaluating scheduling algorithms. Depending on the benchmarks’ purpose they could consist of individual tasks, full applications, or even complete systems where specific software and hardware combinations are considered together.

A key theme in the discussion was the importance of designing benchmarks that reflect actual real-time workloads and applications. Real-time systems span diverse domains and benchmarks should reflect this diversity. Instead of relying exclusively on small code fragments, participants suggested a potential shift towards specification-based benchmarks: defining the intended behavior rather than a fixed implementation, with the goal of deriving implementations that exhibit predictable worst-case performance.

Domains that are particularly representative of modern real-time systems include vision and perception (e.g., camera or LIDAR input), sensor fusion, control algorithms such as model-predictive control, and mixed workloads running on heterogeneous architectures (e.g., involving both CPUs and GPUs). These domains may feature execution time variation depending on the nature of the input data, a characteristic that existing benchmark suites largely fail to capture.

Several participants pointed to tools like Simulink and Lustre as valuable sources for generating realistic benchmarks. Simulink, in particular, includes many example controllers that are already central to real-world safety-critical systems. These models can be used to generate C code, with support for different code generation configurations, including full closed-loop systems that simulate both controllers and plants. Similarly, code generated from Lustre, or real-world code bases like Autoware, could serve as useful starting points for building a more diverse and representative benchmark suite.

Another important aspect raised was the need to define reference contexts for benchmarks. This includes specifying the hardware architecture and microarchitecture, selecting reasonable parameter values, and ideally providing baseline results obtained using known analysis tools. Benchmarks should also include annotations – such as loop bounds – to ensure they are compatible with WCET analysis tools like AbsInt.