节点文献
DDS并行模型及其形式化
Parallel Model of DDS and Its Formalization
【摘要】 DDS(deadline-driven scheduler)模型是实时系统研究中的一个经典模型,但其原始设置中未提及空间因素.在DDS模型的原始设置上进行扩展,给出了DDS并行模型并在该模型设置下研究带空间限制的任务调度问题.提出了极大空间相容组的概念,并给出了全局调度算法和该算法可行的条件.最后还引入分离逻辑的思想对时段演算进行扩充,得到了新的形式系统DC*,利用DC*把DDS并行模型形式化.
【Abstract】 Although the model of DDS (deadline-driven scheduler) is a classical model of real-time system, the space-condition is not included in its original framework. Based on the extension of the original framework of DDS, multi-processes task scheduling with space-constraint is investigated. By studying the parallel model of DDS, the concept of maximal separated task-set, the primary scheduling algorithm and the general scheduling algorithm are presented. In order to formalize the parallel model of DDS, the paper extend duration calculus to DC* with the idea of separation logic, which can express the space-constraint successfully, and give the formalization too.
【Key words】 parallel model of DDS; general scheduling algorithm; separation logic; duration calculus; formalization;
- 【文献出处】 软件学报 ,Journal of Software , 编辑部邮箱 ,2009年06期
- 【分类号】TN74
- 【被引频次】4
- 【下载频次】222