The concept of a probabilistic worst-case execution time (pWCET) has gradually emerged from the work of many authors over the course of 2–3 decades. Intuitively, pWCET is a simplifying model abstraction that safely over-approximates the ground-truth probabilistic execution time (pET) of a real-time task. In particular, when analyzing the cumulative processor demand of multiple jobs, the pWCET abstraction is intended to allow for the use of techniques from probability theory that require random variables to be independent and identically distributed (IID), even though the underlying ground-truth pET random variables are usually not independent. However, while powerful, the pWCET concept is subtle and difficult to define precisely, and easily misinterpreted. To place the pWCET concept on firm, unambiguous mathematical foundations, this paper proposes the first rigorous, axiomatic definition of pWCET that is suitable for formal proof. In addition, an adequacy property is stated that formally captures the intuitive notion of an “IID upper bound on pET.” The proposed pWCET definition is shown to satisfy this adequacy condition, and thereby is the first notion of pWCET for which the IID guarantee is formally established. All definitions and proofs have been verified with the Coq proof assistant.

Estimating the worst-case deadline failure probability (WCDFP) of a real-time task is notoriously difficult, primarily because a task's execution time typically depends on prior activations (i.e., history dependence) and the execution of other tasks (e.g., via shared inputs). Previous analyses have either assumed that execution times are probabilistically independent (which is unrealistic and unsafe), or relied on complex upper-bounding abstractions such as probabilistic worst-case execution time (pWCET), which mask dependencies with pessimism. Exploring an analytically novel direction, this paper proposes the first closed-form upper bound on WCDFP that accounts for dependent execution times. The proposed correlation-tolerant analysis (CTA), based on Cantelli's inequality, targets fixed-priority scheduling and requires only two basic summary statistics of each task's ground- truth execution time distribution: upper bounds on the mean and standard deviation (for any possible job-arrival sequence). Notably, CTA does not use pWCET, nor does it require the full execution-time distribution to be known. Core parts of the analysis have been verified with the Coq proof assistant. Empirical comparison with state-of-the-art WCDFP analyses reveals that CTA can yield significantly improved bounds (e.g., a lower WCDFP than any pWCET-based method for ~70% of the workloads tested at 90% pWCET utilization and 60% average utilization). Beyond accuracy gains, the favorable results highlight the potential of the previously unexplored analytical direction underlying CTA.

Response-time analysis (RTA) is a key technique for the analysis of (not only) safety-critical real-time systems. It is hence crucial for published RTAs to be safe (i.e., correct), but historically this has not always been the case. To ensure the trustworthiness of RTAs, recent work has pioneered the use of formal verification. The Prosa open-source project, in particular, relies on the Coq proof assistant to mechanically check all proofs. While highly effective at eradicating human error, such formalization and automatic validation of mathematical reasoning still faces barriers to more widespread adoption as most researchers active today are not yet accustomed to the use of proof assistants. To make this approach more broadly accessible, this paper presents a case study in the verification of a novel RTA for sporadic tasks under FIFO scheduling using the Coq proof assistant. The RTA is derived twice, first using traditional, intuition-based reasoning, and once more formally in a style that highlights the similarity to the intuitive argument. The verified RTA is of interest in itself: experiments with synthetic workloads based on an automotive benchmark show the new RTA to clearly outperform a prior RTA for FIFO scheduling. The paper further explores the performance of FIFO scheduling relative to traditional fixed-priority and earliest-deadline-first approaches, showing that FIFO scheduling can benefit lower-rate tasks.

Robots are commonly subject to real-time constraints. To ensure that such constraints are met, recent work has analyzed the response times of processing chains under ROS 2, a popular robotics framework. However, prior work supports only scalar worst-case execution time bounds and does not exploit that the ROS 2 scheduling mechanism is starvation-free.This paper proposes a novel response-time analysis for ROS 2 processing chains that accounts for both the high execution-time variance typically encountered in robotics workloads and the starvation freedom of the default ROS 2 callback scheduler. Experimental results from both synthetic callback graphs and a real ROS 2 workload empirically show the proposed analysis to be much more accurate (often by a factor of 2× or more).

Determining a soft or firm real-time task’s probabilistic worst-case response time is a central goal when quantifying and bounding the probability of deadline misses, but current approaches are either (i) fast, but coarse-grained analytical bounds without precision guarantees, (ii) based on convolution and suffer from high space and time complexity, or (iii) combine convolution with resampling techniques that accrue pessimism in an uncontrolled manner. As a new alternative, this paper provides the first probabilistic response-time analysis method based on Monte Carlo simulation, which provides a controlled trade-off between analysis runtime, the desired degree of accuracy, and the permissible probability of a misestimate. An evaluation shows the proposed Monte Carlo analysis to routinely provide more accurate worst-case deadline failure probability (WCDFP) estimates than prior approaches, especially when considering large task sets (where prior methods struggle). In particular, it is shown to scale to workloads with up to 500 tasks while achieving one to three orders of magnitude better precision than analytical or convolution-based approaches (given an equivalent time budget).

The purpose of a response-time analysis (RTA) is to obtain safe bounds on the worst-case response times of all critical tasks in a real-time system. To this end, the system is described with a mathematical model (typically, comprising a workload model, a resource model, and a scheduling policy), which is then analyzed to derive response-time bounds. This procedure requires (i) a theory that rigorously justifies that the RTA correctly characterizes the worst-case scenario, and (ii) an RTA tool that executes the concrete calculations.

This paper introduces the first general and rigorous formalization of the classic busy-window principle for uniprocessors. The essence of the principle is identified as a minimal set of generic, high-level hypotheses that allow for a unified and general abstract response-time analysis, which is independent of specific scheduling policies, workload models, and preemption policy details. From this abstract core, the paper shows how to obtain concrete analysis instantiations for specific uniprocessor schedulers via a sequence of refinement steps, and provides formally verified response-time bounds for eight common schedulers and workloads, including the widely used fixed-priority (FP) and earliest-deadline first (EDF) scheduling policies in the context of fully, limited-, and non-preemptive sporadic tasks. All definitions and proofs in this paper have been mechanized and verified with the Coq proof assistant, and in fact form the common core and foundation for verified response-time analyses in the Prosa open-source framework for formally proven schedulability analyses.

Ethernet is expected to play a key role in the development of the next generation of safety-critical distributed real-time systems. Unfortunately, the use of switched Ethernet in place of traditional field buses such as CAN exposes systems to the risk of Byzantine errors (or inconsistent broadcasts) due to environmentally-induced transient faults.Byzantine fault tolerance (BFT) protocols can mitigate such errors to a large extent. However, no BFT protocol has yet been investigated from the perspective of hard real-time predictability. Classical Byzantine safety guarantees (e.g., 3f+ 1 processes can tolerate up to f Byzantine faults) are oblivious to non-uniform fault rates across different system components that arise due to environmental disturbances. Furthermore, existing analyses abstract from the underlying network topology despite its strong influence on actual failure rates.In this work, we present (i) a hard real-time interactive consistency protocol that allows distributed processes to agree on a common state despite Byzantine errors; and (ii) the first quantitative, real-time-aware reliability analysis of such a protocol deployed over switched Ethernet in the presence of stochastic transient faults. Our analysis is free of reliability anomalies and, as we show in our evaluation, can be used for a reliability-aware design space exploration of different fault tolerance alternatives.