AI 中文总结
本研究针对安全关键系统的EDF调度器实现，提出基于演绎式验证的Frama-C/ACSL框架，验证其满足三项核心正确性属性，成功应用于RTEMS 5、RTEMS 6及FreeRTOS的EDF扩展。
AI 中文摘要
实时操作系统（RTOS）依赖调度器实现来提供可预测的任务执行。对于安全关键系统而言，仅对抽象调度策略进行推理是不够的，具体实现也必须保留预期的调度语义。这对最早截止期优先（EDF）调度来说尤其具有挑战性，因为EDF引入的、由截止期派生的动态优先级，常通过复用原本为固定优先级调度设计的内核基础设施来实现。本研究通过最早截止期优先（EDF）调度器的任何实现都必须满足的三个基本属性，形式化了EDF的正确性。基于这些属性，我们提出了一个采用演绎式验证的框架，该框架适用于任何基于EDF的调度器实现。我们在Frama-C/ACSL中实例化该框架，并将其应用于三种结构不同的EDF调度器实现：RTEMS 5、RTEMS 6和FreeRTOS的EDF扩展。
英文摘要
Real-Time Operating Systems (RTOSes) rely on scheduler implementations to provide predictable task execution. For safety-critical systems, it is therefore not sufficient to reason only about the abstract scheduling policy; the concrete implementation must also preserve the intended scheduling semantics. This is particularly challenging for Earliest Deadline First (EDF) scheduling, because EDF introduces dynamic, deadline-derived priorities that are often realized by reusing kernel infrastructure originally designed for fixed-priority scheduling. In this work, we formalize EDF correctness through three essential properties that any implementation of the Earliest Deadline First (EDF) scheduler must satisfy. Based on these properties, we propose a framework utilizing deductive verification, that applies to any EDF-based scheduler realization. We instantiate the framework in Frama-C/ACSL and apply it to three structurally different EDF scheduler realizations: RTEMS 5, RTEMS 6, and an EDF extension of FreeRTOS.
