An Intuitive Formal Proof for Deadline Driven Scheduler

ZHAN Naijun. An Intuitive Formal Proof for Deadline Driven Scheduler[J]. Journal of Computer Science and Technology, 2001, 16(2).

Citation:

ZHAN Naijun. An Intuitive Formal Proof for Deadline Driven Scheduler[J]. Journal of Computer Science and Technology, 2001, 16(2).

Citation:

ZHAN Naijun. An Intuitive Formal Proof for Deadline Driven Scheduler[J]. Journal of Computer Science and Technology, 2001, 16(2).

Abstract

This paper presents another formal proof for the correctness of theDeadline Driven Scheduler (DDS). This proof is given in terms ofDuration Calculus which provides abstraction for random preemption ofprocessor. Compared with other approaches, this proof relies on manyintuitive facts. Therefore this proof is more intuitive, while it isstill formal.

FullText(HTML)

Export File