A formal proof of the deadline driven scheduler

Abstract

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 [1], and the scheduler that we select here to serve as an example is the Deadline Driven Scheduling Algorithm [2]. 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.