RefinedProsa: Connecting Response-Time Analysis with C Verification for Interrupt-Free Schedulers

RefinedProsa: Connecting Response-Time Analysis with C Verification for Interrupt-Free Schedulers

연구 분야: Verification

학회: Proceedings of the ACM on Programming Languages, Volume 9, Issue PLDI

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.