DDS并行模型及其形式化  

Parallel Model of DDS and Its Formalization

作　　者：刘真环[1,2] 韦立[2,3] 陈艳[2] 赵荣盛[2] 王驹[4] 

机构地区：[1]桂林空军学院教研部,广西桂林541003 [2]广西师范大学数学科学学院,广西桂林541004 [3]贵州大学计算机科学与技术学院,贵州贵阳550025 [4]广西师范大学计算机科学与信息工程学院,广西桂林541004

出　　处：《软件学报》2009年第6期1406-1413,共8页Journal of Software

基　　金：国家自然科学基金Nos.60573010;60663001;广西研究生教育创新计划No.2007106020701M52~~

摘　　要：DDS(deadline-driven scheduler)模型是实时系统研究中的一个经典模型,但其原始设置中未提及空间因素.在DDS模型的原始设置上进行扩展,给出了DDS并行模型并在该模型设置下研究带空间限制的任务调度问题.提出了极大空间相容组的概念,并给出了全局调度算法和该算法可行的条件.最后还引入分离逻辑的思想对时段演算进行扩充,得到了新的形式系统DC*,利用DC*把DDS并行模型形式化.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.

关 键 词：DDS并行模型 全局调度算法 分离逻辑 时段演算 形式化 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]