[2026年7月29日提交]

查看PDF HTML（实验性）

摘要：实时操作系统（RTOS）依赖调度器实现来提供可预测的任务执行。对于安全关键系统，仅对抽象调度策略进行推理是不够的；具体实现也必须保留预期的调度语义。这对最早截止期限优先（EDF）调度尤其具有挑战性，因为EDF引入了基于截止期限的动态优先级，这些优先级通常通过重用原本为固定优先级调度设计的内核基础设施来实现。在这项工作中，我们通过EDF调度器必须满足的三个基本属性来形式化EDF的正确性。基于这些属性，我们提出了一个利用演绎验证的框架，适用于任何基于EDF的调度器实现。我们在Frama-C/ACSL中实例化了该框架，并将其应用于三种结构不同的EDF调度器实现：RTEMS 5、RTEMS 6以及FreeRTOS的EDF扩展。

提交历史

来自：Jian-Jia Chen [查看邮件]
[v1] 2026年7月29日 星期三 13:56:07 UTC (177 KB)