%0 Journal Article
%T An Intuitive Formal Proof for Deadline Driven Scheduler
%A Zhan Naijun
%A <br>詹乃军
%J 计算机科学技术学报
%D 2001
%I 
%X 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.
%K duration calculus
%K deadline driven scheduler
%K real-time<br>处理机
%K 程序机
%K 持续时间算法
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=F57FEF5FAEE544283F43708D560ABF1B&aid=215A3F6E5B82CE2D3CB7EBAE3510AAAE&yid=14E7EF987E4155E6&vid=7801E6FC5AE9020C&iid=0B39A22176CE99FB&sid=2B25C5E62F83A049&eid=2B25C5E62F83A049&journal_id=1000-9000&journal_name=计算机科学技术学报&referenced_num=0&reference_num=6