Deductive Verification for Earliest Deadline First Scheduler Implementations Daniel Kuhse∗ , Junjie Shi∗ , Jan Duy Thien Pham∗ , Kay Heider∗ , Marcus Völker† , Kuan-Hsun Chen‡ , Jian-Jia Chen∗† ∗ TU Dortmund University, Germany
arXiv:2607.26927v1 [cs.OS] 29 Jul 2026
{daniel.kuhse, junjie.shi, jan.pham, kay.heider}@tu-dortmund.de † RWTH Aachen University, Germany [email protected], [email protected] ‡ University of Twente, The Netherlands [email protected]
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. The verification confirms that the considered implementations satisfy the EDF correctness properties under explicitly stated assumptions on kernel infrastructure. Index Terms—EDF Scheduling, Formal Verification, Real-Time Systems, Real-Time Operating Systems
I. I NTRODUCTION Real-time systems play an indispensable role in modern computing, where timely and predictable responses are crucial across various domains, such as aerospace, automotive, medical devices, and industrial control. In these contexts, Real-Time Operating Systems (RTOSes) act as the backbone, managing hardware resources and ensuring that real-time tasks are executed within their specified deadlines. Ensuring scheduler correctness requires more than proving the abstract scheduling theory. Even when a scheduling policy is well understood mathematically, the corresponding implementation may deviate from the intended semantics because of legacy APIs, implementation optimizations, or interactions with existing kernel data structures. This is particularly relevant for widely used open-source RTOSes such as FreeRTOS [2], Zephyr [30] and RTEMS [40], . Unlike clean-slate kernels such as seL4 [24] and CertiKOS [19] which are designed from the ground up for formal verification, they are developed and maintained over long periods and often evolve by extending existing kernel infrastructure. Formal
verification of scheduler implementations in these existing RTOS is therefore important, but difficult: the verification must account for implementation-level data structures and function interactions while remaining modular enough to be applicable to real systems. This work focuses on Earliest Deadline First (EDF) scheduling. EDF has been extensively studied and is optimal for preemptive uniprocessor scheduling under classical assumptions. Unlike fixed-priority scheduling, however, EDF assigns priorities dynamically according to absolute deadlines: jobs with earlier deadlines must receive higher scheduling priority. This creates additional implementation complexity. A job release may require recomputing a deadline-derived priority, propagating this value through internal priority structures, repositioning the job in the ready queue, and triggering a preemption decision. If any of these steps is missed or performed in the wrong order, the implementation may violate EDF semantics even though the high-level scheduling policy is conceptually simple. In practice, EDF support is often built on top of kernel infrastructure that was not originally designed for dynamicpriority scheduling. For example, RTEMS realizes EDF through its existing priority-management and scheduler-node infrastructure. FreeRTOS, by contrast, does not provide EDF scheduling by default, so an EDF scheduler must be introduced by modifying its fixed-priority scheduling infrastructure. These implementations illustrate a common challenge: EDF correctness is not confined to the task-selection policy alone, but depends on the consistent maintenance of deadlinederived priorities across task releases, ready-queue updates, and scheduler decisions. Implementation optimizations further amplify this problem. For example, Zephyr uses _kernel.ready_q.cache to cache the next job to execute, avoiding repeated ready-queue searches. As reported in [1], incorrect maintenance of this cache can lead to unintended execution orders. Specifically, due to this design choice, each job must update its absolute deadline before being added to the ready queue, as no further deadline updates are permitted once the job is in the queue unless the _kernel.ready_q.cache is explicitly refreshed.
Such cases show that documentation and programming discipline alone are insufficient: EDF correctness must be verified across the interactions between deadline updates, ready-queue state, and scheduler decisions. At the same time, comprehensive verification of existing RTOS kernels is difficult. Current verification tools must cope with legacy APIs, lowlevel data structures, and implementation-specific control flow. A modular verification strategy is therefore commonly used: individual components are verified under explicit assumptions about the correctness of the surrounding kernel infrastructure. Existing verification efforts address related aspects, but do not fully cover this problem. Some approaches develop verified kernels or scheduler components within verificationoriented frameworks, such as seL4 [24] and CertiKOS [19]. Vanhems et al. [41] proposed a formal proof methodology for EDF scheduling by reimplementing the scheduler, rather than directly verifying the existing implementations. Other approaches focus on existing RTOSes, but verify selected APIs, abstract scheduler models, or applications running on top of RTOS semantics. For example, Liang et al. [28] verify 22 API functions in the FreeRTOS scheduling module. However, it lacks a systematic framework for reasoning about the correct composition of these functions. The deductive framework proposed in [38] targets FreeRTOS applications under cooperative (non-preemptive) scheduling. It relies on a formal encoding of FreeRTOS scheduling semantics and therefore verifies application behavior with respect to this encoding. However, these works do not verify how EDF scheduling is realized inside the scheduler infrastructure of existing RTOS implementations. This is important because EDF correctness is not confined to the task-selection policy alone: it also depends on how deadline-derived priorities are represented, propagated, and maintained across scheduler nodes, ready queues, and task release operations. Our Contribution: In this work, we propose a general framework for verifying the correctness of EDF scheduler implementations in existing RTOSes. To the best of our knowledge, this is the first work to present a formal verification framework applicable to EDF scheduler implementations in existing RTOSes. The main challenges lie in identifying correctness properties, formalizing them within a general framework, and addressing the reuse of generic kernel primitives not originally designed for dynamic-priority scheduling. The contributions of this work are summarized as follows: • We analyze the general operational workflow of EDF schedulers in RTOSes and formally define three key correctness properties, deadline priorities, ready queue management, and scheduler decisions, that any correct implementation must satisfy. • We propose a deductive verification framework for formally verifying EDF scheduler implementations against the three defined correctness properties under clearly stated assumptions. • We validate the framework across various EDF scheduler realizations, including RTEMS 5 and RTEMS 6 (Sec. V). We also modify a standard FreeRTOS V11.1.0 to support
Periodic Release Manager
Tasks
Task Creation
deadline calculation
P1: Deadline priorities
P2: Ready queue mgmt.
Jobs
Ready Queue
deadline-based priority update
order updates
P3: Scheduler decisions Priority-based Preemptive Scheduler
dispatch
Data Structure
Processor
Fig. 1. The workflow of EDF scheduler. The gray area is the verification target in this work. Each block marks the area relevant to a property.
EDF scheduling and subsequently verify it (Sec. VI). This demonstrates portability across evolving and structurally distinct RTOS infrastructures. We make our verification effort including the ACSL annotations, FreeRTOS modification and replication instructions available as an artifact [25].1 II. BACKGROUND In this section, we first introduce the task model assumed in this work. We then describe the fundamental principles of the EDF scheduling algorithm. Finally, we provide a formal definition of the key properties that any correct EDF scheduler implementation must satisfy. A. Periodic Task Model We consider the implemented scheduler is employed on a uni-processor system for a set of N tasks T = {τ1 , . . . , τN }. Each task is described by τi = (Di , Ti ), where: • Ti is the period of task τi . • Di is the relative deadline of τi . All tasks release an infinite number of task instances, called jobs. Each job is characterized by a tuple Jiℓ = (τi , riℓ , dℓi ). For the ℓ-th job, ℓ ∈ N: riℓ is the release time, i.e., riℓ = ℓ×Ti , and dℓi is the absolute deadline, i.e., dℓi = riℓ + Di . Please note that the worst-case execution time (WCET) Ci of task τi is not relevant to the EDF scheduler’s operation and is thus omitted from the system model. Let the ready queue Q(t) = {J1 , J2 , . . . , Jn } be a list of jobs sorted in non-decreasing order of their absolute deadlines. Any two jobs Jiı , Jjȷ ∈ Q(t) must satisfy the following condition: if Jiı precedes Jjȷ in Q(t), then dıi ≤ dȷj . If dıi = dȷj , then Jiı must be released earlier than Jjȷ . In addition, the schedule function S : N → J ∪ {⊥} maps each time t to the job J executing at time t, or ⊥ if the processor is idle. B. EDF Scheduling Workflow and Core Components Preemptive EDF scheduling guarantees that, at any moment, the job with the earliest absolute deadline among all ready jobs is selected for execution. Figure 1 illustrates the general operational workflow of an EDF scheduler, abstracted across RTOS implementations. The process begins with task creation. The 1 https://github.com/TU-Dortmund-CS-LS12-DAES-teaching/ edf-verification
2
Periodic Release Manager handles task activations by generating jobs at each release point, computing absolute deadlines, and assigning priorities accordingly. Afterwards, released jobs are inserted into the ready queue with deadline-based ordering. The Priority-Based Preemptive Scheduler monitors the queue and the currently executing job, performing preemptions when a new job arrives with an earlier deadline. While the core scheduling principle is well-defined, its realization in RTOS kernels can vary significantly due to legacy design choices, internal API constraints, and systemlevel optimizations. Despite these differences, most EDF implementations share three core functionalities, including: • Priority assignment: EDF is a job-level dynamic-priority scheduler that assigns priorities to jobs of real-time tasks based on their absolute deadlines, i.e., the earlier the deadline, the higher the priority. When adopting RTOS routines designed for fixed-priority scheduling, priorities of real-time tasks are calculated and updated whenever a new job arrives. • Ready queue management: The ready queue holds all ready jobs ordered by the deadline-derived priorities established above. Whenever a job’s priority is assigned or changes, the queue is updated accordingly, so that the head is consistently the job with the earliest absolute deadline in the ready queue. • Preemptive EDF scheduling: On job arrivals, completions, or priority changes, the scheduler selects the head of the ready queue, i.e., the job with the earliest deadline, for execution. EDF operates in a preemptive manner. That is, if a newly released job has an earlier deadline than the currently running preemptible job, it immediately preempts the executing job. This triggers a context switch. When multiple jobs in the ready queue share the same priority (i.e., identical absolute deadlines), the scheduling order is implementation-defined. For example, in the RTEMS implementation, tie-breaking is resolved using FIFO semantics, i.e., the job enqueued earlier is given the higher priority.
set of ready jobs with priorities as established by Property 1, and yields its minimum-priority element correctly. Property 3: Scheduler decisions (P3). Whenever the ready queue is modified, the scheduler selects arg minJ∈Q(t) dJ from the ready queue. If the running job is preemptible and some ready job has an earlier deadline, a context switch is scheduled. All of these properties are local to the scheduler. We assume that the context switch is executed immediately after the scheduler finishes the selection of the highest-priority job2 . If this assumption does not hold, the implementation results in a significant gap between the selection of the highestpriority job and the actual context switch. This requires an additional verification to ensure that the ready queue is not updated between the end of the scheduler and the start of the subsequent context switch. To establish this would require covering all interrupt handlers and OS infrastructure. This is a broader verification effort related to the correctness of the scheduler of the RTOS itself in addition to its EDF variant, and thus out of scope for this work. Combined these properties establish Definition 1. Property 1 and Property 2 together ensure that the ready queue includes all ready jobs with their priorities assigned to their deadlines and the head being the job with the earliest deadline. Property 3 ensures that after returning from any scheduler entry point the running job has the earliest deadline or a context switch is scheduled. Under the previously discussed assumption for the context switch execution, it is then guaranteed that on exiting the interrupt routine, the running job has the earliest deadline. III. G ENERAL EDF S CHEDULING S TRUCTURES This section outlines the key components required for EDF scheduling: the task model, periodic release manager, jobs, ready queue, and priority-based preemptive scheduler. 1) Tasks: A task represents a long-lived software entity in an RTOS, typically defined at system configuration time. Tasks encapsulate application-level control flows and may be periodic, sporadic, or aperiodic. In EDF scheduling, tasks themselves do not carry static priorities; rather, they act as templates for generating jobs, which are assigned dynamic priorities based on their absolute deadlines. Each task is associated with a set of configuration parameters that determine its timing behavior, i.e., τi = (Di , Ti ). These configurations are typically specified during system initialization but may be updated during runtime to accommodate dynamic system behavior. Each task is represented internally using a Task Control Block (TCB), which stores configuration data and runtime information such as next release time and pointers to pending jobs. 2) Periodic Release Manager: The Periodic Release Manager (PR Manager) is responsible for generating jobs according to the temporal behavior specified by each task, including periodic, sporadic, or event-driven releases. It enforces the
C. Formal Properties Required for EDF Scheduler We formalize the correctness of EDF scheduling as a single property over the externally observable state, and introduce a set of supporting subproperties that together establish it. Definition 1. Earliest Deadline First. A preemptive EDF scheduler implementation is correct if, at every observable time point t outside the scheduler, the currently running job Jr implies that either 1) Jr has the earliest absolute deadline among the set of eligible jobs Q(t) ∪ {Jr }, or 2) a context switch has been scheduled and will execute before the next observable point outside the scheduler. To establish Definition 1, we identify three properties that any correct EDF implementation must satisfy: Property 1: Deadline priorities (P1). For every job, its absolute deadline is mapped to its scheduling priority. Property 2: Ready queue management (P2). The ready queue is updated according to scheduling events to reflect the
2 This property holds in FreeRTOS because the context switch is called immediately after the scheduler. For RTEMS, the context switch is deferred until the thread dispatch disable level returns to zero.
3
timing constraints of tasks and ensures that job creation aligns with the system’s real-time requirements. For each periodic task, the PR Manager maintains a release schedule, typically driven by a system timer. When a release condition is met, the PR Manager generates a new job instance, computes its absolute deadline, derives the corresponding EDF priority, and inserts the job into the ready queue. 3) Jobs: A job is a runtime instantiation of a task, characterized by a specific arrival time and absolute deadline. During execution, jobs transition between scheduler-visible states such as Ready, Executing, and Blocked, depending on dispatch decisions and synchronization events. From the scheduler’s perspective, each job release triggers a sequence of ready-queue updates, dispatch decisions, and potential preemption events that determine whether EDF ordering semantics are preserved. For example, a running job may be preempted and returned to the Ready state if another job with an earlier absolute deadline becomes runnable. In EDF scheduling, a job’s priority is determined by its absolute deadline, with earlier deadlines corresponding to higher priority (i.e., lower numerical values in typical RTOS encodings). Each job maintains scheduler-relevant attributes including its arrival time, absolute deadline, dynamic priority, and links required for ready-queue management. 4) Ready Queue: The ready queue holds all jobs that are ready to execute. Independent of the underlying implementation (e.g., red-black trees or sorted linked lists), EDF correctness requires that queue ordering consistently reflects deadline-derived priorities. The ready queue provides the following core operations: • Inserting a newly released or preempted job with its computed priority; • Updating a job’s position when its deadline changes; • Retrieving the job with the earliest deadline (the head of the queue) for scheduling decisions. The correctness and efficiency of the ready queue are critical to ensuring timely and predictable scheduling behavior. 5) Priority-Based Preemptive Scheduler: The prioritybased preemptive scheduler selects and dispatches the job with the highest priority (i.e., earliest deadline) for execution. It continuously monitors job arrivals, completions, and priority changes to determine whether a context switch is required. Key operations include: • Comparing the priority of a newly released or updated job with that of the currently running job; • Initiating preemption when a new job has a higher priority, triggering a context switch; • Dispatching the job with the earliest deadline from the ready queue when the processor is idle or when the current job completes; • Performing context switches: saving the state of the current job, enqueuing it back into the ready queue, and restoring the context of the next job. The scheduler ensures that the job with the earliest deadline always gains processor access, faithfully enforcing EDF scheduling semantics.
IV. F ORMAL V ERIFICATION F RAMEWORK FOR EDF S CHEDULER This section presents a verification framework targeting the core components of EDF scheduler implementations in RTOSes using Frama-C. In contrast to the approach of [41], which verifies a reimplemented EDF scheduler built on newly designed primitives, our goal is to formally verify existing implementations embedded within RTOS kernels, potentially relying on generic infrastructure not originally intended for EDF scheduling. A. Deductive Verification In order to verify the properties of the EDF scheduler implementation, we apply deductive verification [13], [22]. For completeness, we briefly review Hoare Logic and ACSL. Hoare Logic provides a systematic framework for rigorously reasoning about program correctness [22]. A key concept is the Hoare Triples, denoted as {P } C {Q}, where: • C is the set of considered instructions in the program. • P is the precondition, describing the state before executing C. • Q is the postcondition, describing the expected state after C’s execution. If the precondition P holds before execution, and C terminates, the postcondition Q must hold afterward. To express these properties, we use the ANSI/ISO C Specification Language (ACSL) [15], which enables the formal specification of function contracts directly in C code. Deductive verification with function contracts is modular: when verifying a function, other called functions are treated as black boxes and only their contracts are considered, unless explicitly inlined. Contracts are embedded using comments (/*@ ... */) and include: • requires for preconditions; • assigns to declare which variables may be modified; • ensures for postconditions; • \valid to specify valid memory regions. ACSL supports predicates which describe properties of the program state, which can be used as pre- and postconditions. For example, a predicate could state that an item is in the ready queue or that the head of the ready queue has the earliest deadline. These predicates can be used to specify intended behavior and express invariants. This way we can formally capture the properties outlined in Section II-C as ACSL contracts, which are then verified against the implementation. B. Frama-C and Memory Model To validate the function contracts, we use Frama-C (Framework for Modular Analysis of C programs) version 32 [11], [14], along with the WP plugin [16] for static analysis and deductive verification. The WP plugin generates proof obligations, i.e., logical formulas derived from the code and its annotations, which are initially simplified using the built-in Qed engine. If Qed cannot fully resolve them, the obligations are passed to an SMT solver via Why3 [6]. In this work,
4
we use Alt-Ergo version 2.6.3 [33] as the backend solver. 1 /*@ Verification is performed at the source-code level, making 2 requires ready_queue_invariant(Q); 3 requires edf_running_earliest(Q); the approach architecture-independent, assuming a conforming 4 ... implementation of lower-level system components. 5 ensures ready_queue_invariant(Q); Accurate verification of C code requires a formal memory 6 ensures edf_running_earliest(Q); 7 ensures \forall Job *j’; model to represent read and write operations, particularly when 8 In(j’, Q) <==> \old(In(j’, Q)) || j’ == j; accessing memory via pointers. We apply the Typed memory 9 */ model [18], which is the standard recommendation and rep- 10 void scheduler unblock(Queue *Q, Job *j); resents memory using global arrays and models pointers as Listing 1. The transition contract on a generic unblock entry point. indices. The \separated predicate allows specifying that two pointers refer to disjoint memory regions, preventing alias- as FreeRTOS delayed/suspended lists and RTEMS prioritying issues and unintended interactions between components. aggregation trees, are modeled in the same way. Stronger We also enable Cast option to support unsafe pointer casts, guarantees could be obtained in future work by verifying these which are often used in system-level code to implement low- data structures or adopting verified alternatives such as priority level abstractions and structural inheritance, necessitating it for search trees [26]. verifying RTEMS and FreeRTOS. Some scheduler decisions are represented through volatile D. Verification Strategy We establish properties 1–3 through two proof artifacts: state, such as pending-dispatch flags or current-task pointers. By default, Frama-C treats each volatile access as potentially 1) predicates to state invariants over the scheduler’s state, yielding a fresh value, which prevents stable reasoning about and 2) function contracts to describe the expected behavsuch variables. To verify Property 3, we thus use Frama- ior of the scheduler’s core components. Key invariants are C’s Volatile option to mirror volatile accesses into proof- maintained across the scheduler’s operations. We give a highonly ghost variables. The soundness of this approach relies level overview of the modeling strategy. Our concrete ACSL on the absence of concurrent modifications during scheduler specifications are very large as they need to account for operations, which is ensured for the uniprocessor scheduler implementation details, so we opt for idealized versions to clearly illustrate the general pattern, with the full specifications entry points considered in our case studies. available in the artifact [25]. C. Verification Boundary and Assumptions The ready queue is modeled as a set of priority nodes Our framework verifies the EDF scheduler against the with predicates describing its state. For example, In(j, Q) properties defined in Section II-C, treating certain parts of the expresses that job j is a member of the ready queue Q, RTOS infrastructure as correct components. The modularity and head_is_earliest(Q) expresses that the minimumof contract-based verification allows us to focus on the core priority element of Q corresponds to the job with the earliest EDF logic. Data structures used by the scheduler are specified absolute deadline. Every scheduler entry point that mutates the ready queue at the verification boundary through contracts. These contracts are assumptions, but a verified replacement could be substi- carries postconditions stating which predicates change and tuted without affecting the EDF proofs. The remaining OS how. Listing 1 illustrates the pattern on a generic unblock operation: a queue well-formedness invariant is maintained, infrastructure is assumed correct implicitly. Correctness of OS infrastructure: We assume the cor- the scheduler decision predicate is re-established: either the rectness of underlying kernel primitives. This includes the running job remains earliest or a dispatch is pending, and dispatch mechanism, memory management, context switching the postcondition states that the only change to the queue’s and the periodic tick infrastructure. None of these are specific membership is the addition of the unblocked job j. We apply this pattern to establish each property as follows. to EDF. For context switching, we additionally assume that a Property 1. An invariant links the scheduler’s effective requested context switch is executed before the next observable point outside the scheduler, with no ready-queue modifications priority back to the job’s deadline, paired with a postcondition on the function that originally sets the deadline. intervening, as discussed in Section II-C. Property 2. Ready-queue management needs to maintain an Correctness of operations on advanced data structures: We treat scheduler data structures as part of the verification invariant that the head of the queue corresponds to the job with boundary and model each ready queue abstractly as a set of the earliest deadline. Operations that modify the queue have priority nodes. Membership predicates and interface contracts postconditions that reflect the expected changes to the queue’s specify insertion, removal, and minimum-element retrieval, al- membership. Moreover, the ready queue must be well-formed, lowing the EDF proof to rely on abstract ready-queue behavior such as correct links between nodes and their TCB. Property 3. Scheduler decisions are captured by a single rather than the concrete data-structure implementation. In the case studies below, this abstraction is instantiated for RTEMS, predicate stating that either the running job has the earliest whose ready queue is implemented using OpenBSD’s red- deadline among all ready jobs, or a dispatch is pending, see black tree, and FreeRTOS, whose ready queue is implemented Listing 2. This predicate is carried as a postcondition on every using a doubly-linked list. Additional scheduler lists, such scheduler entry point.
5
Preemptive scheduler
Scheduler EDF Node node
m pa
po sit i
re
on
Scheduler Node Base
Base.priority
re
Priority Aggregation
co
d pr dl-b io as rit e y d
release/ cancel job
n m ew in im um
/*@ predicate edf_running_earliest(Queue *Q) = 2 dispatch_scheduled || 3 (\forall Job *j; In(j, Q) ==> 4 running_job->deadline <= j->deadline); 5 */ 1
node.priority
RB Tree-based Ready Queue
RB Tree
Listing 2. Scheduler predicate for the ready queue, global running job.
V. V ERIFICATION OF THE EDF SCHEDULER IN RTEMS
Fig. 2. The ready queue management workflow within EDF scheduler node in RTEMS implementation.
Through the proposed framework, we conduct a case study on the EDF scheduler implementation in RTEMS 5 and 6, focusing on the scheduler module and relevant _Thread functions. We give an overview of the EDF implementation, outline the preprocessing steps, summarize key EDF-related functions, and explain their verification objectives.
Beyond the job release, cancellation, priority update and schedule functions, the EDF scheduler provides block, unblock and yield entry points which modify the ready queue and potentially trigger scheduling decisions. These interactions between legacy priority-management infrastructure, scheduler-node updates, ready-queue manipulations and the internal mechanisms constitute the primary verification targets in this work. Both RTEMS 5 and 6 share the same overall architecture and workflow, with the main difference being in the internal mechanisms, with some of the EDF-specific dispatch logic being refactored into general uniprocessor scheduling helpers in RTEMS 6.
A. EDF Implementation Overview The RTEMS scheduling infrastructure is built around a base scheduler node that stores job-specific metadata required for scheduling decisions. These decisions are triggered by events such as job completions and ready-queue updates. A base node includes a priority aggregation, which maintains a redblack tree of all active priority nodes associated with it. A priority node captures an individual priority contribution to the thread, for example from the scheduler itself, an EDF deadline, or synchronization-related priority inheritance. This allows RTEMS to combine priority contributions from different sources, such as EDF deadlines and synchronizationrelated priority adjustments. Each scheduling algorithm extends this base node with algorithm-specific data structures. In the EDF scheduler, the node is augmented with an embedded red-black-tree node used to link the corresponding thread into the EDF ready queue. It also contains an additional priority field that caches the minimum priority obtained from the priority aggregation tree. Figure 2 illustrates this structural relationship. In RTEMS, job priority assignment, determined by its absolute deadline, is managed by the PR manager under the implicit-deadline assumption (∀τi , Di = Ti ) adopted in the default implementation. Notably, the implementation relies on legacy APIs prefixed with rate monotonic, which were originally designed for fixed-priority scheduling, to handle job releases and deadline updates. Following the workflow outlined in Figure 2, priority updates triggered by job releases or cancellations propagate through several layers before affecting dispatch decisions: The deadline is mapped to a priority in a priority node, the priority aggregation is updated, and the effective priority in the base node is potentially updated. If the effective priority changes, a pending update is recorded, denoting that the scheduler node’s priority cache must be updated. When the scheduler node is updated, its position in the ready queue is adjusted. The schedule function then potentially leads to a new thread heir, the thread that will be dispatched next, and signaling a deferred context switch. The PR manager calls both the release and cancel, as well as the potentially needed scheduler priority update functions.
B. Setup and Source Code Processing The applied version of Frama-C includes machdep support for GCC extensions, accommodating compiler-specific constructs used in RTEMS, such as empty structs and flexible array members. We employ the corresponding RTEMS crosscompiler, x86_64-rtems5/6-gcc, and select the AMD64 Board Support Package (BSP), the BSP available for x86_64 in RTEMS, supporting a uniprocessor configuration. The EDF scheduler in RTEMS relies on the tree.h library from OpenBSD, which provides the red-black tree implementation used for ready queue management and priority aggregation within scheduler nodes. As shown in Section IV-C, we assume the correctness of this data structure by describing the behavior of its interface through contracts, abstracting its state as a set of nodes with associated predicates. We verify the EDF Scheduler module, including its entry points, underlying mechanisms such as priority aggregation and ready-queue management, and the periodic release manager’s release/cancel function. The gray-shaded region in Figure 1 highlights the scope of the verification focused in this work. We provide abstract models for the ready queue and priority aggregation, state key invariants and helper lemmas, and annotate all relevant functions up to the RB-tree boundary. Verification is performed per entry point; contracts of internal functions are refined iteratively until all proof obligations are discharged. C. Verification Target We outline the target of our verification, which encompasses the EDF scheduler module, underlying priority aggregation and ready queue mechanisms and the periodic release manager’s release/cancel operations. Together, their contracts and their corresponding invariants establish the properties P1-P3.
6
trigger priority update
set deadline
- Releasing Job - Cancelling Job
_Release_job _Cancel_job
Thread functions _add _change _remove
releasing or canceling job
modify priorities
EDF Scheduler
PR Manager
Actions: _Thread_Priority_{changed|add|remove}
_Update_priority _Schedule _Yield _Block/_Unblock
_Thread_Priority_apply _Thread_Priority_do_perform_actions: _Priority_{Changed|Non_empty_insert|Extract_non_empty}
Fig. 3. Overview of verified EDF scheduler and thread priority functions, with prefixes omitted. Internal helpers are verified, but only entry points are shown. Yellow highlights deadline to priority propagation, while blue highlights core scheduling operations.
_Thread_queue_Context_add_priority_update
Fig. 4. Control flow of modifying the base scheduler nodes priority fields.
We categorize the relevant functions and invariants into two groups based on their roles in the EDF scheduling mechanism. The first group relates to the priority management and update pipeline (P1) as detailed in Section V-D, while the second group focuses on the ready queue management and scheduling operations (P2-P3) given in Section V-E. Figure 3 visually distinguishes these groups, using yellow for the first and blue for the second, though we note that update priority touches on all three properties. We establish certain general structural properties as invariants, such as consistency of links between an EDF node and its thread, that are not directly related to the EDF-specific logic but are necessary for the overall correctness of the implementation. Beyond these, invariants are grouped by their role in the priority management pipeline or the scheduling operations, as detailed below. Deadline priorities (P1): In the PR Manager flow, the pathway for both job release and cancellation begins with either EDF’s release or cancel function. When a job is released or canceled, it is necessary to modify the priority fields in its base scheduler node, ensuring that the priority aligns with the current absolute deadline. Based on an abstract model of the priority aggregation, we establish the following: • A postcondition on the release function ensures that the priority node’s priority field is correctly set according to the job’s absolute deadline (and, if not present, inserted into the aggregation tree). (P1) • An invariant establishes that the priority in the base scheduler node is the minimum of all priority nodes in the aggregation tree. (P1) • Another invariant ensures that the EDF scheduler node’s priority field is consistent with the base node’s priority or that an update priority call is pending to restore it. (P1) These properties are verified for EDF’s release, cancel entry points and the periodic release manager’s release/cancel functions. For the periodic release manager, it is also ensured that the priority update is executed. Preemptive scheduling (P2-P3): For the scheduler, readyqueue updates and heir selection are triggered by thread state changes (block, unblock, yield, priority update) and explicit scheduling calls. The scheduler must ensure: the ready queue is correctly updated, and the thread heir is correctly set.
Based on an abstract model of the ready queue, we establish the following: • A postcondition on the unblock/block/yield functions ensures that the thread’s EDF node is correctly added to or removed from the ready queue, and that the ready queue’s state is updated accordingly as defined by the abstract model. (P2) • An invariant that holds after every EDF entry point ensures that if the current heir is preemptible, it is the earliest ready job. (P3) • Another invariant that holds after every EDF entry point, stating that if the current heir is not the executing thread, a dispatch is pending. (P3) These properties are verified for the EDF update priority, unblock, block, yield and schedule entry points, as well as helper functions like initialization and update heir. D. Verification for Deadline-Driven Task Prioritization This subsection verifies Property 1. Figure 4 provides an overview. All functions in this flow up to the RB-tree boundary have been annotated with ACSL contracts and verified. In RTEMS, each thread (or job) contains a priority aggregation tree that represents all the priority entries and extracts the highest priority of the current job. The job release or cancellation process involves one of the following three _Thread functions: • _Thread_Priority_changed is used when the priority node is already part of the internal priority aggregation tree, necessitating an update to reflect the changes. • _Thread_Priority_add handles the addition of a new priority to the aggregation tree. • _Thread_Priority_remove is responsible for removing an existing priority from the tree. Afterwards, the _Thread_Priority_apply function is called with an associated priority action type. Each action type influences the specific tree operation during the red-black tree’s internal update. It encapsulates both the priority node and the priority action type into a single object. This object is then utilized by the _Thread_Priority_do_perform_actions function, resulting in one of two possible outcomes:
7
If the tree operation introduces a new minimum priority, it influences the task’s positioning within the ready queue, so the scheduler node must be updated to reflect this new minimum value and an update action enqueued. • If the tree operation does not result in a new minimum priority, no further action is required. After inserting the priority into the tree (if it exists), the _Thread_queue_Context_add_priority_update function is called if a new minimum priority value emerges. The purpose is to enqueue the task into a scheduler queue for subsequent updating. In principle, this priority update could also be propagated to other priority aggregations due to e.g. synchronization-related priority adjustments. However, on the release/cancel path, the thread has to be either executing or ready, and this is therefore a noop. The underlying priority combinators used for aggregation modification, _Priority_{Non_empty_insert, Changed, Extract_non_empty}, are each verified against the abstract aggregation model under the RB-tree interface assumptions, exhibiting the expected new-minimum or no-new-minimum behavior. •
Pending update
_Thread_Priority_update
_Scheduler_EDF_Update_priority
Update cached priority, reinsert
_Scheduler_EDF_Schedule
Update heir
Fig. 5. Control flow of executing priority update. Pending updates come from Fig. 4. Internal helpers for RTEMS 5/6 differ.
A. Preliminary Setup Before describing the FreeRTOS scheduling infrastructure and our EDF modifications, we first clarify the FreeRTOS variant used in this case study. This setup is necessary because FreeRTOS is split into a portable kernel layer and a hardwarespecific porting layer. Practical ports may contain platformspecific scheduler code or assembly routines that are outside the scope of Frama-C verification. The kernel layer provides the functionality needed by an RTOS to manage, schedule and execute tasks. The porting layer interfaces with a specific hardware platform, for example by providing the implementation of the periodic tick interrupt and context-switching routines. However, many ports such as the FreeRTOS port for the Espressif ESP32 microcontrollers [12] are highly optimized for the specific platform by implementing parts of the scheduler in assembly code and integrating platform-dependent code into kernel-level scheduling paths. As Frama-C is not able to verify assembly code and modifications to the FreeRTOS kernel are necessary to provide an EDF scheduler, such official platform-specific distributions are not directly suitable for our verification purpose. Hence, we modified a generic FreeRTOS V11.1.0 kernel to support EDF scheduling. As a hardware platform we use a Texas Instruments MSP430FR5994 microcontroller [39] and provide a corresponding FreeRTOS port. Our version keeps all scheduling-relevant operations in C, making the resulting EDF scheduler amenable to verification with Frama-C. We include our port of FreeRTOS for the MSP430FR5994 alongside our modifications to support EDF scheduling as part of the artifact [25].
E. Verification for Preemptive EDF Scheduling Operations In this subsection, we detail the EDF scheduler operations establishing Property 2 and Property 3. The unblock, block, yield, schedule and update-priority entry points each update the ready queue and/or trigger an heir update. We focus on _Scheduler_EDF_Update_priority as the representative example. Following the previously described priority change from release or cancel, _Thread_Priority_update checks for any pending priority updates, and if so, invokes the EDF update priority function for affected nodes. We have verified that the PR Manager’s release and cancel functions correctly exhibit this behavior, updating both the base and EDF scheduler node priorities when needed. This updates the cached priority field in the EDF scheduler node and adjusts the ready queue accordingly. If the new priority is earlier than the current heir’s and the heir is preemptible, preparations for a context switch are initiated. This involves updating the thread heir, i.e., the pointer to the next processor owner scheduled for execution. This procedure is illustrated in Figure 5. Postconditions include all the previously mentioned invariants and that the priority update is correctly reflected in the EDF scheduler node. VI. V ERIFICATION OF EDF S CHEDULING IN F REE RTOS
B. Scheduling Infrastructure
To further evaluate the applicability of the proposed framework, we conduct a second case study on an EDF scheduler implementation in FreeRTOS. Unlike RTEMS, FreeRTOS provides a lightweight fixed-priority scheduling infrastructure by default, and EDF scheduling therefore requires kernel-level modifications. We describe the verification-oriented FreeRTOS setup, summarize the EDF-related scheduler changes, and explain their verification objectives.
In general, FreeRTOS makes no distinction between jobs and tasks. Hence, there is only ever exactly one task instance that is either executing, ready, or blocked. By default, FreeRTOS uses static priorities that are assigned to each task at task creation. All information about a task is stored in its corresponding TCB object. The TCB however contains no information about task periods or deadlines. In general,
8
FreeRTOS has no notion of explicit deadlines. A deadline in FreeRTOS is always assumed to be implicit and is only checked whenever a task has finished its execution. To realize periodic tasks, FreeRTOS uses the xTaskDelayUntil() function, where the task’s period is supplied as a function parameter. This function first determines the next release time of the task. Then, if the next release time has not already passed, the task’s deadline is not violated and the task is inserted into the global delayed list, sorted by its next release time. Finally, the task yields, i.e., the scheduler is invoked to context switch to the next highest priority task. If the task has missed its deadline, the task stays in the ready queue. For the scheduling behavior considered in this work, the relevant task states are represented primarily by ready lists and delayed lists. Tasks that are ready to be executed are stored in the ready list and tasks that are blocked until a later time unit are stored in a global delayed list3 . In standard FreeRTOS, the ready list is kept sorted by the static priorities of the tasks, while the delayed list is sorted by the next release time of any task contained therein. A common FreeRTOS idiom for implementing periodic tasks is to use xTaskDelayUntil() together with the periodic tick interrupt, which iterates through the global delayed list and moves any task that becomes ready at the current tick count to the ready list, and performs a scheduling decision. The fixed-priority scheduler always selects the head element in the global ready list as the currently running task. The currently executing task is denoted by a global variable pxCurrentTCB that points to the task’s TCB. At any point outside of the scheduler, the currently executing task is pointing to the head element of the ready list. Whenever a task gets released to the ready list, the scheduler determines if the currently running task is still the head element. If that is no longer the case, a context switch to the task at the head of the ready list is performed.
Therefore, we integrate the setting of the new deadline into the xTaskDelayUntil() function to exploit the period parameter as the relative deadline. As a result, we force implicit deadlines. Third, the xDeadline field must be respected by the scheduler whenever it is invoked. That means, when a task is inserted to the ready list, the xDeadline is used as the sorting criterion. For a sorted insertion into a list, FreeRTOS uses an internal list item field in the TCB. This field usually contains the next release time of the task, as a sorted insertion by default only occurs when a task is added to the delayed list. We only replace the list item value by the xDeadline prior to the insertion to the ready list, such that the ready list is kept sorted after the current absolute deadlines of the tasks. Besides these modifications, all internal functions where the scheduler had previously used the static task priorities for comparing which task to execute are modified to take the current absolute deadlines into account. The overall architecture of the FreeRTOS scheduler remains unchanged. D. Verification Target We outline our verification target for the EDF scheduler in FreeRTOS. As described in Section VI-A, our FreeRTOS variant keeps all scheduling-relevant operations in C. We therefore cover the tick increment, delay, suspend, resume, and task-switch selection functions, together with their underlying helper functions. Together, the verified contracts and invariants establish Properties 1–3. As in the RTEMS case study (Section IV-C), we treat the list module as a correct component. Similarly, we also use Frama-C’s Volatile option to reason about the dispatch flag. However, in addition to the dispatch flag, several other global variables such as the current TCB pointer and the delayed list are also volatile in FreeRTOS, requiring us to operate under the same scheme for them. Deadline priorities (P1): As no priority aggregation mechanism is used, P1 involves only two aspects: 1) the delay function correctly sets the deadline and 2) maintaining an invariant that ensures that the deadline field in the TCB corresponds to the value in the ready list item field used for sorting. This invariant is maintained across all entry points. Ready queue management (P2): We establish invariants that ensure the ready, delay and suspend are well-formed and disjoint lists, and that the ready and delay list have their head pointing to the minimum element. We combine these invariants into a single scheduler context invariant that is maintained across all entry points. The lists are correctly updated in the delay, suspend and resume functions, with e.g. all jobs that become ready during a tick being moved from the delayed list to the ready list. To ensure this we use loop invariants. Scheduler decisions (P3): The task switch function correctly selects the task with the earliest deadline and updates pxCurrentTCB accordingly when the scheduler is running or sets a dispatch pending flag. An invariant is maintained across all entry points that the current TCB has the smallest deadline among all ready tasks (or that the dispatch flag is set).
C. EDF Scheduling in FreeRTOS A straightforward way to retrofit EDF scheduling into FreeRTOS is to preserve the existing list-based scheduling architecture and replace static priorities by absolute deadlines as the scheduling key. This requires modifications to three central parts of the kernel: the task metadata stored in the TCB, the update of timing information in xTaskDelayUntil(), and the ready-list ordering used by the scheduler. First, the current absolute deadline of a task must be stored. For this, we replace the static priority field of the TCB by a current absolute deadline field xDeadline. Consequently, when a task is created, the value supplied in place of the original static priority denotes the task’s initial absolute deadline. Second, the xDeadline must be updated before the next time that the task will be released. Since we do not add any additional fields to the TCB to keep its original size, we can only rely on one value that stores the current absolute deadline. 3 FreeRTOS also maintains additional lists, such as overflow delayed lists for tick-count wraparound. These mechanisms are part of the original kernel infrastructure and are not specific to our EDF modification.
9
In the tick ISR, the task switch is immediately triggered after the tick increment call, ensuring that afterwards the current TCB is always the task with the earliest deadline when the scheduler is not suspended. Finding. Updating the deadline in xTaskDelayUntil() is natural because the function computes the next release time and receives the period parameter. Our verification, however, revealed an overrun case: If a task calls xTaskDelayUntil() after its next release time has already passed, FreeRTOS keeps the task in the ready list instead of delaying it. Under fixed-priority scheduling this is harmless. Under EDF, however, updating xDeadline while the task remains in the ready list may invalidate the ready-list ordering, thereby violating P1 and P2. The verified fix is to reinsert the task into the ready list whenever an overrun causes the task to remain ready after its deadline update.
TABLE I D ERIVED PROOF GOALS AND REQUIRED TIME OF RTEMS VERIFICATION ( EACH ENTRY: RTEMS 5 / RTEMS 6). Proof Goals Qed
5/5 0/0 19/14 2/3 10/10 21/17 64/62 133/130 82/81 14/55 39/38 39/39 12/3 339/337
4.9/5.0 s 0.8/0.8 s 8.6/5.1 s 3.6/3.9 s 4.3/4.5 s 10.8/12.6 s 23.5/35.0 s 51.6/51.7 s 30.1/29.9 s 84.6/15.2 s 30.9/33.4 s 23.2/27.3 s 28.9/26.0 s 401.6/152.1 s
1584/1722 779/794
707.5/402.6 s
Initialize 10/10 Node_initialize 15/15 Block 41/42 Schedule 13/19 Yield 30/35 Unblock 67/81 Update_priority 139/166 Release_job 144/148 Cancel_job 157/156 Thread_Priority_{*} 119/189 RM_Release_job 67/69 RM_Cancel 69/73 Scheduler helpers 88/84 Priority helpers 625/635 Total
VII. R ESULTS AND D ISCUSSIONS The proposed framework was applied to multiple EDF scheduler realizations, including RTEMS 5, RTEMS 6, and FreeRTOS. Across these implementations, the verification focused on the three core EDF correctness properties defined in Section II-C: deadline-driven task prioritization, ready queue management, and preemptive scheduling behavior. The verification sources and the setup for reproducing the evaluation tables are available in our artifact [25].
Approx. Time
Alt-Ergo
TABLE II D ERIVED PROOF GOALS AND REQUIRED TIME OF F REE RTOS VERIFICATION . Proof Goals Qed
A. Verification Results
Approx. Time
Alt-Ergo
vTaskSwitchContext 32 vTaskSuspend 45 vTaskResume 40 xTaskDelayUntil 60 xTaskIncrementTick 98 Task helpers 154
2 25 21 44 43 21
1.1 s 11.9 s 4.8 s 44.6 s 44.7 s 14.3 s
Total
156
121.4 s
For RTEMS and FreeRTOS, the verification confirms that the EDF scheduler implementations satisfy Properties 1-3 under the assumptions of Section IV-C. • P1: In RTEMS, the priority pipeline maps every deadline change at job release/cancel into the minimum of the aggregation tree and propagates it into the EDF scheduler node. In FreeRTOS, xTaskDelayUntil refreshes xDeadline at every release, and an invariant ties the ready-list sort key to it. • P2: In RTEMS, all ready-queue mutations preserve the ready-queue model with the earliest-deadline job at the head and correctly insert and remove jobs. In FreeRTOS, the context invariant ensuring valid ready, delayed and suspended lists, is preserved by every verified entry point and correctly moves jobs between the lists. • P3: In RTEMS, schedule picks the earliest-deadline ready job as heir and requests a context switch when the running thread is preemptible. In FreeRTOS, the tick ISR ensures the EDF property holds unless the scheduler is suspended, while other functions preserve the EDF property or request a dispatch.
RTEMS family this structural reuse extended to many contracts, as RTEMS 5 and RTEMS 6 share the same general scheduler architecture, with their differences mainly in an internal refactoring and internal helpers. FreeRTOS applies the methodology on a substantially different infrastructure, with several doubly linked lists and no clear API boundary between the scheduler and the underlying data structure manipulation. The same methodology and overall strategies for approaching the correctness properties were applicable, but more proof engineering was required to find fitting data structure invariants and contracts to work around these differences. The derived proof goals for both built-in Qed and selected proofs to Alt-Ergo, and required time of all covered parts of the verification of RTEMS 6, RTEMS 5 and FreeRTOS, via Frama-C and wp, are presented in Table I and Table II, respectively. The process was executed with 24 threads on an AMD Ryzen 9 3900X with 64 GB main memory.
B. Verification Effort and Reusability
C. Practical Considerations for Source-Level Verification
The framework carried across all three case studies at the structural level: the three correctness properties and invariants maintaining them, the abstract-data-structure boundary, and specific strategies like the ghost-mirroring discipline for volatile scheduler flags applied without change. Within the
Applying deductive verification directly to RTOS source code requires bridging the gap between solver-friendly specifications and low-level implementation idioms. In our case studies, the main challenges arise from pointer-based data structures, unsafe casts, and macro-heavy kernel code. They
10
429
are handled through explicit verification boundaries, auxiliary contract clauses, and proof-oriented wrappers where needed. First, ACSL can express separation between memory regions, but proving separation properties over larger data structures such as multiple linked lists is often difficult for the solver. For instance, in FreeRTOS, modifying the delayed list should preserve predicates over the ready list. Although this can be specified by separating the reachable elements of the two lists, the solver does not always establish automatically that such separation preserves list-level properties across list manipulations. We thus state preservation conditions explicitly in the contracts of list operations, requiring properties of untouched lists to remain unchanged. In the same way, in RTEMS we annotate internal helpers with explicit preservation postconditions, leading to at times verbose contracts and more manual proof effort. For the RM functions, it was necessary to mark the update queue as a static global, as Frama-C was not able to verify that deallocating the empty update queue from the stack did not affect the ready queue. This does not alter the behavior in the non-SMP case. Second, system-level C code often uses casts to implement low-level abstractions and structural reuse. As discussed in Section IV-B, the selected Frama-C memory model supports such casts, but does not itself prove that every cast preserves the intended structural interpretation. Accordingly, our verification treats the correctness of these representation assumptions as part of the trusted boundary of the source code. Finally, FreeRTOS makes extensive use of macros for list operations. Since Frama-C verifies preprocessed C code and ACSL contracts cannot be attached directly to macros, we introduce proof-only wrapper functions for the relevant macro calls. These wrappers provide explicit contracts while preserving the original implementation semantics. The required source-level adaptation is therefore minimal and limited to making existing operations visible to the verifier.
protokernel [23]. These approaches provide strong correctness guarantees, but they usually require the scheduler or kernel to be developed within a verification-oriented framework. There is currently no way to use these methods to verify existing schedulers or new schedulers implemented in existing RTOS kernels. Given the widespread use of existing RTOS implementations, this therefore presents a significant gap in the state of the art for applying these verification techniques to real-world systems. The second approach focuses on existing RTOS implementations, which is the focus of this work. Model checking has been used to analyze RTEMS, Trampoline/OSEK, ARINC 653 systems, partitioned RTOS models, Contiki, and FreeRTOS scheduler/interrupt behavior [7], [17], [29], [31], [36], [37]. Specifically, Gadia et al. [17] modeled RTEMS code in Java and verified it using Java Pathfinder. Lin and Wang [29] analyzed the FreeRTOS scheduler on ARM Cortex-M4 cores by modeling both the scheduler and the relevant interrupt mechanisms. These approaches are effective for finding subtle design errors, but may suffer from state-space explosion and often verify translated or abstracted models rather than the source implementation directly [3], [17]. To reduce the gap between the verified artifact and the implementation, deductive verification [13], [22] can be used to verify source code directly against formal specifications. This approach is supported by tools such as VerCors [5], VCC [10] and Frama-C [11]. VCC has been used to verify parts of the Microsoft Hyper-V hypervisor [27], while Frama-C has been applied to safety-critical embedded software such as the Paparazzi UAV autopilot [34]. In the RTOS context, Chong and Jacobs [9] formally verified the interprocess communication mechanism of FreeRTOS. Tasche et al. [38] proposed a deductive-verification approach for cooperative FreeRTOS applications using VerCors, combining an encoding of FreeRTOS semantics with automatically generated reachable abstractstate invariants. Shi et al. [35] introduced a Frama-C-based framework for resource synchronization protocols, studying the implementations in RTEMS. These works demonstrate the applicability of deductive verification to RTOS-related software, but they do not target the verification of EDF scheduler implementations in existing RTOS kernels.
VIII. R ELATED W ORK Providing a verified RTOS can be approached in two main ways. The first approach is to develop a new RTOS, or key RTOS components, together with formal correctness proofs. For complete operating-system kernels, representative efforts include the verification of the seL4 microkernel in Isabelle/HOL [24], which required parts of the microkernel to be manually reimplemented for verification. Gu et al. [19] presented CertiKOS, a framework for building concurrent operating-system kernels whose layers are verified in Coq [4]. Guo et al. [20], [21] further connected verified schedulability analysis with CertiKOS using the Proven Schedulability Analysis (PROSA) framework. Scheduler-specific verification has also been studied in this line of work. Vanhems et al. [41] proposed a formal proof methodology for an EDF scheduler. They first prove the correctness of the election function in Coq and then lift this proof to the implementation level through refinement steps into a shallow embedding of a subset of C, which is then translated to C using the Digger tool, running on top of the Pip
Other verification approaches address related but distinct aspects of operating-system correctness. Nicole et al. [32] developed a fully automated verification process for small OS kernels at the binary level, ensuring the absence of privilege escalation and runtime errors. However, this approach does not verify whether the implementation satisfies high-level functional properties derived from the scheduler design. Some formal methods focus on timing or schedulability analysis rather than implementation correctness. For instance, Bozhko et al. [8] established a formal foundation for the busy-window principle through an abstract response-time analysis independent of specific scheduling policies and workload models, with all definitions and proofs mechanized in the Coq proof assistant.
11
IX. C ONCLUSION In this work, we proposed a general framework for verifying the correctness of EDF scheduler implementations in existing RTOSes. We formally defined three correctness properties that all EDF schedulers must satisfy. These properties capture the fact that EDF correctness is not limited to selecting the earliest-deadline job, but also depends on the consistent propagation and maintenance of deadline-derived priorities across scheduler data structures and task release operations. We applied the framework to the uniprocessor EDF scheduler in RTEMS 5, RTEMS 6 and FreeRTOS, performing the first deductive verification under explicitly stated assumptions on kernel infrastructure and data-structure operations. We release our verification effort as an artifact [25]. The FreeRTOS case study further demonstrates the usefulness of the framework by exposing an overrun-related edge case in a straightforward EDF retrofit, where updating a task’s deadline without reinserting it into the ready list may violate the ready-queue ordering. The results show that our framework can be applied to EDF scheduler logic in legacy or repurposed RTOS infrastructures without re-engineering the entire kernel.
[11] P. Cuoq, F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles, and B. Yakobowski. Frama-c: A software analysis perspective. In Software Engineering and Formal Methods SEFM. Springer, 2012. [12] Espressif Systems. ESP-IDF Programming Guide. https://docs.espressif. com/projects/esp-idf/en/v6.0.1/esp32/index.html, Last accessed on 202605-20. [13] R. W. Floyd. Assigning meanings to programs. Proceedings of Symposium on Applied Mathematics, 19:19–32, 1967. [14] FRAMA-C. Frama-C Software Analyzers. https://frama-c.com/, Last accessed on 2026-05-06. [15] FRAMA-C. ANSI/ISO C Specification Language, 2007. https://frama-c. com/html/acsl.html, Last accessed on 2026-05-15. [16] FRAMA-C. WP Plugin, 2007. https://frama-c.com/fc-plugins/wp.html, Last accessed on 2026-05-15. [17] S. Gadia, C. Artho, and G. Bloom. Verifying nested lock priority inheritance in RTEMS with java pathfinder. In 18th International Conference on Formal Engineering Methods, Proceedings, 2016. [18] C. Garion, G. Hattenberger, B. Pollien, P. Roux, and X. Thirioux. A gentle introduction to c code verification using the frama-c platform, 2022. [19] R. Gu, Z. Shao, H. Chen, X. N. Wu, J. Kim, V. Sjöberg, and D. Costanzo. Certikos: An extensible architecture for building certified concurrent OS kernels. In 12th OSDI, 2016. [20] X. Guo, M. Lesourd, M. Liu, L. Rieg, and Z. Shao. Integrating formal schedulability analysis into a verified OS kernel. In Computer Aided Verification - 31st International Conference, CAV. Springer, 2019. [21] X. Guo, L. Rieg, and P. Torrini. A generic approach for the certified schedulability analysis of software systems. In Embedded and Real-Time Computing Systems and Applications (RTCSA). IEEE, 2021. [22] C. A. R. Hoare. An axiomatic basis for computer programming. Commun. ACM, 12(10):576–580, 1969. [23] N. Jomaa, P. Torrini, D. Nowak, G. Grimaud, and S. Hym. Prooforiented design of a separation kernel with minimal trusted computing base. Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 76, 2018. [24] G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, et al. sel4: Formal verification of an os kernel. In Operating systems principles, 2009. [25] D. Kuhse, J. Shi, J. D. T. Pham, K. Heider, M. Völker, K.-H. Chen, and J.-J. Chen. Deployment Instructions and Function Contracts for Deductive Verification of Earliest Deadline First Scheduler Implementations, 2026. https://github.com/TU-Dortmund-CS-LS12-DAES-teaching/ edf-verification, Last accessed on 2026-07-27. [26] P. Lammich and T. Nipkow. Priority search trees. Arch. Formal Proofs, 2019. [27] D. Leinenbach and T. Santen. Verifying the microsoft hyper-v hypervisor with vcc. In FM 2009: Formal Methods, pages 806–809, 2009. [28] H. Liang, D. Zhang, X. Pei, X. Jia, G. Li, and J. Xu. A correctness verification method for c programs based on vcc. In International Conference on Cyber Security and Cloud Computing. IEEE, 2016. [29] C. Lin and B. Wang. Formal analysis of freertos scheduler on ARM cortex-m4 cores. In International Conference on Formal Engineering Methods, pages 199–215, 2024. [30] Linux Foundation. Zephyr project. https://zephyrproject.org/, 2016. Last accessed on 2026-05-26. [31] H. Mousavi, A. Ebnenasir, and E. Mahmoudzadeh. Formal specification, verification and repair of contiki’s scheduler. ACM Trans. Cyber Phys. Syst., 7(4):22:1–22:28, 2023. [32] O. Nicole, M. Lemerre, S. Bardin, and X. Rival. No crash, no exploit: Automated verification of embedded kernels. In 27th IEEE Real-Time and Embedded Technology and Applications Symposium, 2021. [33] OCamlPro SAS. An SMT Solver For Software Verification. https: //alt-ergo.ocamlpro.com/, Last accessed on 2026-05-20. [34] B. Pollien, C. Garion, G. Hattenberger, P. Roux, and X. Thirioux. Verifying the mathematical library of an uav autopilot with frama-c. In 26th International Conference FMICS. Springer, 2021. [35] J. Shi, C. von Egidy, K. Chen, and J. Chen. Formal verification of resource synchronization protocol implementations: A case study in RTEMS. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2022. [36] A. Singh, M. D’Souza, and A. Ebrahim. Conformance testing of ARINC 653 compliance for a safety critical RTOS using UPPAAL model checker. In SAC: The 36th ACM/SIGAPP Symposium on Applied Computing, pages 1807–1814. ACM, 2021.
ACKNOWLEDGMENTS This result is part of a project (PropRT) that has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement No. 865170). This work has received funding from the DFG Priority Program “Disruptive Memory Technologies” (SPP 2377) as part of the project “ARTS-NVM” (502308721). It is further supported by the DFG Project “One-Memory” (405422836). R EFERENCES [1] Alexander Pinheiro Paschoaletto. Potential Issues with the EDF Scheduler in Zephyr, 2024. https://github.com/zephyrproject-rtos/zephyr/ issues/79361, Last accessed on 2026-05-06. [2] Amazon. FreeRTOS: Real-time operating system for microcontrollers. https://www.freertos.org/, Last accessed on 2026-05-18. [3] C. Baier and J.-P. Katoen. Principles of model checking. MIT press, 2008. [4] Y. Bertot and P. Castéran. Interactive Theorem Proving and Program Development - Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2004. [5] S. Blom and M. Huisman. The vercors tool for verification of concurrent programs. In FM: Formal Methods - 19th International Symposium, Singapore, May 12-16, 2014. Proceedings, pages 127–131, 2014. [6] F. Bobot, J.-C. Filliâtre, C. Marché, and A. Paskevich. Why3: Shepherd your herd of provers. Boogie 2011: First International Workshop on Intermediate Verification Languages, 2011. [7] K. Boukir, J. Béchennec, and A. Déplanche. Requirement specification and model-checking of a real-time scheduler implementation. In 28th International Conference on Real Time Networks and Systems, RTNS, pages 89–99. ACM, 2020. [8] S. Bozhko and B. B. Brandenburg. Abstract response-time analysis: A formal foundation for the busy-window principle. In M. Völp, editor, 32nd Euromicro Conference on Real-Time Systems, ECRTS, LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. [9] N. Chong and B. Jacobs. Formally verifying freertos’ interprocess communication mechanism. In Embedded World Exhibition & Conference, 2021. [10] E. Cohen, M. Dahlweid, M. A. Hillebrand, D. Leinenbach, M. Moskal, T. Santen, W. Schulte, and S. Tobies. VCC: A practical system for verifying concurrent C. In Theorem Proving in Higher Order Logics, 22nd International Conference, Proceedings. Springer, 2009.
12
[37] S. Staroletov. A formal model of a partitioned real-time operating system in promela. Proceedings of the Institute for System Programming of RAS, 32:49–66, 12 2020. [38] P. Tasche, P. Herber, and M. Huisman. Deductive verification of cooperative RTOS applications. ACM Trans. Embed. Comput. Syst., 24(5s):131:1–131:25, 2025. [39] Texas Instruments Incorporated. MSP430FR599x, MSP430FR596x Mixed-Signal Microcontrollers, 2021. [40] The RTEMS Project. Real-Time Executive for Multiprocessor Systems (RTEMS), 2014. http://www.rtems.org/, Last accessed on 2026-05-27. [41] F. Vanhems, V. Rusu, D. Nowak, and G. Grimaud. A formal correctness proof for an EDF scheduler implementation. In 28th IEEE Real-Time and Embedded Technology and Applications Symposium, RTAS, 2022.
13