This paper presents a formalization in the duration calculus (DC) of
scheduling policies for tasks with shared resources.  Two frameworks
are presented for specifying classes of schedulers.  With these
specifications, some properties of these schedulers were proved using
the formal deduction of DC.  This paper aims to encourage other
researchers to formally treat real-time aspects of operating systems
which in the past were conventionally a piece of ad hoc territory in
computer science.