程序正确性验证不仅是计算机科学界一直关注的一个重要问题,也是推动计算机科学发展的主要动力之一。分离逻辑是此问题研究下出现的新研究领域,它是一个用来对关于共享可变数据结构的程序进行推理的逻辑系统,其主要的特征是支持局部推理。时段演算是一个用于嵌入式实时软件系统设计的演算系统,即在设计嵌入式实时软件系统时,用该形式语言来描述软件需求和特征,并且通过推理验证来保证最终的软件产品是否满足这些需求和具备这些特征。当前对实时任务调度理论的研究很少考虑到空间的约束,往往只考虑实时限制,但在许多实际问题中,(比如铁路交叉口控制、网络服务的拥塞问题、城市交通的指挥问题、软件系统资源共享问题等等)中,空间是一个不可忽视的因素。时段演算是规约实时系统的一个强有力工具,然而它几乎没有考虑空间因素;分离逻辑较好地解决了空间共享问题,但它不能够较好地解决并发程序的同步问题。由此,在时段演算中引入空间概念显得极为必要,我们采用的方法是在时段演算中引入空间变量,这为我们规约实时问题中的空间共享与空间分离提供了方便。本文从一些现实问题的背景中抽象出SLDDS模型,并研究此模型里的调度问题,最后考虑这个模型的形式化问题。本文的主要内容安排如下:序言,介绍分离逻辑,时段演算的研究现状和本文的出发点。第1章,介绍基础分离逻辑。第2章,介绍时段演算。第3章,先将DDS模型扩充为更一般的SLDDS问题,重新审视Liu-Layland定理,给出此类实时问题离散化的理论基础,然后研究SLDDS模型里的调度问题。第4章,先介绍我们所要用到的语言,然后初步给出该模型的形式化。本文主要理论结论如下:定理1给定一个SLDDS问题Q , Q是可调度的当仅当存在对Q的一个划分: }使得所有的长条{d_i×a_i | 1≤i≤n可以满足如下要求放入长方块D×1中:(ⅰ)所有长条都是垂直而不重叠地;(ⅱ)来自d_i×W_i的任何两个小长条一个不能在另一个的上方,即对来自某个d_i×W_i的所有小长条,通过长方块D×1底边上任何点的垂线至多穿过其中一个的中间。定理2 SLDDS问题Q有解的充要条件是存在[0, 1]上的一个阶梯函数f (t ),使:是一个符号表达式并且每个di至多在其中出现一次若否在则t处d在f t的形式表达式中出现定理3在SLDDS模型中,SLEDF调度算法是最优的。即若一个SLDDS问题是可调度的,则它是SLEDF可调度的。