摘要
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.
基金
UNU/IIST, and was done during the author's stay at UNU/IIST(July 1998 to August 1999), and partially supported by the National
