An intuitive formal proof for Deadline Driven Scheduler |
| |
| Authors: | Naijun Zhan |
| |
| Affiliation: | (1) Laboratory of Computer Science and Technology, Institute of Software, The Chinese Academy of Sciences, 100080 Beijing, P.R. China |
| |
| Abstract: | 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. |
| |
| Keywords: | duration calculus deadline driven scheduler real-time |
| 本文献已被 CNKI 维普 万方数据 SpringerLink 等数据库收录！ |
| 点击此处可从《计算机科学技术学报》浏览原始摘要信息 |
|
点击此处可从《计算机科学技术学报》下载免费的PDF全文 |
