An Intuitive Formal Prooffor Deadline Driven Scheduler  

作　　者：詹乃军 

出　　处：《Journal of Computer Science & Technology》2001年第2期146-158,共13页计算机科学技术学报（英文版）

基　　金：UNU/IIST, and was done during the author's stay at UNU/IIST(July 1998 to August 1999), and partially supported by the National

摘　　要：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.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.

关 键 词：duration calculus deadline driven scheduler REAL-TIME 

分 类 号：TP319[自动化与计算机技术—计算机软件与理论]