Deductive Verification for Earliest Deadline First Scheduler Implementations

arXiv (Cornell University)

Abstract

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.

Authors 7

1. Daniel Kuhse

   TU Dortmund University

   Affiliation as printed

   TU Dortmund University , Germany

2. Junjie Shi

   TU Dortmund University

   Affiliation as printed

   TU Dortmund University , Germany

3. Jan Duy Thien Pham
4. Kay Heider

   TU Dortmund University

   Affiliation as printed

   TU Dortmund University , Germany

5. Marcus Völker Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University , Germany

6. Kuan-Hsun Chen

   University of Twente

   Affiliation as printed

   University of Twente , The Netherlands

7. Jian-Jia Chen Aachen

   TU Dortmund University · RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University , Germany

   TU Dortmund University , Germany