Formal development of real-time priority-based schedulers

We introduce a deductive method for constructing real-time scheduling programs, based on continuous action systems and the higher-order logic of the refinement calculus. The schedulability goal is a guarantee that all the tasks meet their deadlines, at run-time. This analysis reduces to checking that "always" temporal properties hold on the task set, by enforcing adequate invariance properties. The initial, conjunctive model of the real-time system is further transformed, through refinement, into a program that obeys a specific scheduling policy. We exemplify our method on the Deadline-Monotonic and the Earliest-Deadline-First algorithms.