Formalizing Real-time Scheduling as Program Refinement

This paper shows how the feasibility of scheduling a real-time program consisting of a number of parallel processes (tasks) can be proved as a step in the refinement of the program from its specification. Verification of this step of refinement makes formal use of methods and results from real-time scheduling theory. Keywords: real-time program; specification; refinement; schedulability; feasibility. 1 Introduction A typical real-time program is required to respond to external events within specified time bounds and so it must be executed on a system that is sufficiently fast. In general, external events may occur at a rate which results in more than one process of the program being simultaneously under execution; if, at any time, there are fewer processors in the system than active processes, scheduling decisions must be taken to allocate processors to processes. Schedulability is the condition under which a scheduler can execute a real-time program on a system and meet its deadlin..