论文摘要
扩充的实时系统和空间推理是当前的两个新兴领域,在理论及工程应用上都有重要作用。实时系统主要研究在给定的约束条件下多任务的调度安排问题,这些任务是有截止期的,也就是完成的最后时限。DDS（Deadline-Driven Scheduler,即截止期优先任务调度法）能够较好的处理单处理器下的调度问题;多处理器环境下的全局调度是近年来的研究热点,Baruah提出的按比例公平分配的PFair（Proportional fair）调度是典型的全局调度技术。空间推理以空间对象的建模、空间知识表示、对象空间关系的表示和推理等为研究内容。其中,RCC（Region Connection Calculus,区域连接演算）是当前优点最多、使用最方便的关于空间位置关系的定性刻画及推理的逻辑系统。Düntsch、李三江等人已经证明BRCC系统的语义就是基于布尔代数的模型（增加了关系C（x,y））,称为关系代数或连接布尔代数。本文独立提出的课题则处于这两个领域的交叉点。在分别介绍两个领域的背景和国际研究现状之后,讨论了对并行调度进行形式化的重要性。文章建立了模块式的CBA语义（Contact Boolean Algebra）,由此建立扩充的BRCC语言及其公理系统,从而实现了对并行调度的形式化刻画工作,对并行调度的有效性、优化调度的存在性的形式推理作了深入研究,其中,模块式的CBA语义及其性质是重点。文章主要成果有:⑴针对一类扩充实时系统是否存在有效调度给出了两种简单的判定算法:改进单纯形法和增强贪心算法。⑵结合工程应用中的“时间片”技术,将数据型（一般为实数）的调度离散化。构建调度问题的CBA模型。⑶在CBA模型的基础上,构建扩充的BRCC语言实现调度问题的形式化。本文的内容安排如下:第1章相关历史背景及本文研究意义第2章扩充后的并行实时系统模型第3章扩充实时系统的可判定性,给出两个判定算法:改进单纯形法及增强贪心算法。第4章空间逻辑知识及BRCC系统第5章在介绍布尔代数之后,给出并行实时系统的CBA语义模型第6章对BRCC语言进行扩充并将调度问题形式化第7章总结及展望