This paper presents an approach to formalizing and proving real-time
properties of schedulers. The formal logic that we propose to use is
the Duration Calculus, and the scheduler that we select here to serve
as an example is the Deadline Driven Scheduling Algorithm.  The
specification and proof of the algorithm are formulated abstractly by
using the Duration Calculus. The result may encourage others to
formally treat more real-time aspects of operating systems which are
conventionally a piece of ad hoc territory in computer science.