There has been a recent upsurge of interest in formal, machine-checked verification of timing guarantees for C implementations of real-time system schedulers. However, prior work has only considered tick-based schedulers, which enjoy a clearly defined notion of time: the time “quantum”. In this work, we present a new approach to real-time systems verification for interrupt-free schedulers , which are commonly used in deeply embedded and resource-constrained systems but which do not enjoy a natural notion of periodic time. Our approach builds on and connects two recently developed Rocq-based systems—RefinedC (for foundational C verification) and Prosa (for verified response-time analysis)—adapting the former to reason about timed traces and the latter to reason about overheads. We apply the resulting system, which we call RefinedProsa , to verify Rössl, a simple yet representative, fixed-priority, non-preemptive, interrupt-free scheduler implemented in C.

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.