An Intuitive Formal Proof for Deadline Driven Scheduler

• 作 者: 詹乃军
• 机 构: Laboratory of Computer Science and Technology, Institute of Software The Chinese Academy of Sciences
• 出 处: 计算机科学技术学报(英文版)
• 发表日期: 2001年2期
• 关键词: Duration Calculus

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