DDS模型是实时系统早期研究中取得的重要成果之一,其具有很强的代表性,很多现实生活中存在的诸如网络拥塞、生产流程调度、交通运输等问题的解决都可以借助该模型。由于DDS模型未考虑空间限制这一约束条件,而在现实生活中,空间却是一个很关键的因素,这就限制了DDS模型在现实工作中的应用。考虑了空间因素后的DDS并行模型能较好地解决这一问题。如果要设计一个大型自动化调度系统,其软件部分首先要解决的,即是如何将问题形式化。传统的时段演算可以很好地对DDS模型进行形式化,但却不能描述加入了空间限制条件的DDS并行模型。注意到分离逻辑能很好地体现空间分离这一概念,本文重点研究了如何将分离逻辑与时段演算相结合,以便更好地对DDS并行模型进行形式化这一课题。文章的主要内容安排如下:第一章:前言,介绍与本文相关的研究历史和现状;第二章:DDS并行模型,完成了数学模型的构建。通过在原始的DDS模型中加入空间限制,允许有多个处理器同时运行,得到DDS并行模型。随后在该模型下给出了极大空间相容组等概念,并且提出了主调度算法和全局调度算法,得出了本文的两个重要结论:定理2.2任给一个极大空间相容组Q,存在Q的主调度算法。定理2.3设为任务集合的一个划分,对每一极大空间相容组,以记为它的主导任务,则全局调度算法可行的充要条件是主导任务组成的任务集合第三章:时段演算(DC)简介,主要介绍时段演算的字母表、形成规则、推理规则等基本逻辑设置;第四章:分离逻辑语言及其应用,系统地给出分离逻辑的语法、语义以及应用实例——运用分离逻辑给出冒泡排序算法的形式证明,说明了分离逻辑在描述空间分离问题时所具有的优势;第五章:DDS并行模型的形式化,首先给出形式化工具DC~*的语法和语义设置,而后在DC~*下实现DDS并行模型的形式化,表明了将分离逻辑引入时段演算后,构建的DC~*系统在描述DDS并行模型问题上的可行性;总结及展望,总结本文并指出了今后研究的方向。