一句话：在 Rocq 中连接 RefinedC 的 C 验证与 Prosa 的响应时间分析，首次机器验证无中断 C 调度器的时序保证。
本文关注实时系统调度器实现时序保证的机器检验验证。此前工作仅处理基于 tick 的调度器，因为这类调度器有明确的时间量子概念；而广泛用于深度嵌入式和资源受限系统的无中断（interrupt-free）调度器缺乏自然的周期时间概念，其验证尚未被覆盖。作者提出一套新方法，基于并连接两个已有的 Rocq 系统：用于基础 C 验证的 RefinedC 和用于已验证响应时间分析的 Prosa，将前者扩展为可推理带时间的 trace，将后者扩展为可推理开销（overheads）。由此得到的系统称为 RefinedProsa。作者将其应用于 Rössl——一个简单但有代表性的、以 C 实现的固定优先级、非抢占、无中断调度器，完成了端到端验证。该工作把底层 C 代码验证与高层响应时间分析打通，为无中断实时调度器的时序正确性提供了机器检验的保证。
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.
@article{paperbot3139,
title = {RefinedProsa: Connecting Response-Time Analysis with C Verification for Interrupt-Free Schedulers},
author = {Kimaya Bedarkar and Laila Elbeheiry and Michael Sammler and Lennard Gäher and Björn Brandenburg and Derek Dreyer and Deepak Garg},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {PLDI},
year = {2025},
doi = {10.1145/3729249}
}