| 本文已被：浏览 5585次 下载 9058次 |
码上扫一扫！ |
|
|
| DDS并行模型及其形式化 |
|
刘真环1,2, 韦立2,3, 陈艳2, 赵荣盛2, 王驹4
|
|
1.桂林空军学院 教研部,广西 桂林 541003;2.广西师范大学 数学科学学院,广西 桂林 541004;3.贵州大学 计算机科学与技术学院,贵州 贵阳 550025;4.广西师范大学 计算机科学与信息工程学院,广西 桂林 541004
|
|
| 摘要: |
| DDS(deadline-driven scheduler)模型是实时系统研究中的一个经典模型,但其原始设置中未提及空间因素.在DDS模型的原始设置上进行扩展,给出了DDS并行模型并在该模型设置下研究带空间限制的任务调度问题.提出了极大空间相容组的概念,并给出了全局调度算法和该算法可行的条件.最后还引入分离逻辑的思想对时段演算进行扩充,得到了新的形式系统DC*,利用DC*把DDS并行模型形式化. |
| 关键词: DDS并行模型 全局调度算法 分离逻辑 时段演算 形式化 |
| DOI： |
| 分类号: |
| 基金项目:Supported by the National Natural Science Foundation of China under Grant Nos.60573010, 60663001 (国家自然科学基金); the Innovation Project of Guangxi Graduate Education of China under Grant No.2007106020701M52 (广西研究生教育创新计划) |
|
| Parallel Model of DDS and Its Formalization |
|
LIU Zhen-Huan,WEI Li,CHEN Yan,ZHAO Rong-Sheng,WANG Ju
|
| 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 |
