A Machine-Checked Proof of the Optimality of a Real-Time Scheduling Policy

. We describe a mechanically-checked proof of the optimality of earliest-deadline-first (EDF) schedulers on periodic tasks accomplished using the Nqthm theorem prover. We present a formalization of the theorem and discuss why the machine-checked proof is both more complex and more reliable than a corresponding informal proof. 1 Introduction Real-time applications often have several required functions with different timing constraints. In a seminal paper for building real-time systems, Liu and Layland introduce abstractions that facilitate real-time application development [4]. Using a simple computation model, they exhibit different real-time scheduling policies that choose which of an application's various tasks to assign a processor and argue that these policies have certain useful properties. One scheduling policy is earliest-deadline-first (EDF), which assigns the processor to a task that has earliest deadline among the tasks that are currently running. An EDF scheduler is optimal..