[Submitted on 29 Jul 2026]

View PDF HTML (experimental)

Abstract:即時作業系統（RTOS）依賴排程器實作來提供可預測的任務執行。對於安全關鍵系統來說，僅針對抽象排程策略進行推理是不夠的；具體的實作也必須保留預期的排程語義。這對於最早截止期限優先（EDF）排程尤其具有挑戰性，因為 EDF 引入了動態、由截止期限衍生的優先權，通常會重複使用原本為固定優先權排程所設計的核心基礎設施。在這項工作中，我們透過 EDF 排程器必須滿足的三個基本屬性來形式化 EDF 的正確性。根據這些屬性，我們提出一個利用演繹驗證的框架，適用於任何基於 EDF 的排程器實作。我們在 Frama-C/ACSL 中實例化該框架，並將其應用於三種結構不同的 EDF 排程器實作：RTEMS 5、RTEMS 6，以及 FreeRTOS 的 EDF 擴充。

Submission history

From: Jian-Jia Chen [view email]
[v1] Wed, 29 Jul 2026 13:56:07 UTC (177 KB)