基于构件的设计方法在信息物理融合系统(Cyber-Physical System, CPS)设计研究中的广泛使用,促进了分层调度分析模型的研究.分层调度分析模型要求能够对构件的一些性质进行抽象和合成.进程代数模型支持模块式的规范说明和模块式的分析验证；这两特点使得把进程代数作为分层调度分析的模型是一个合适的选择.资源供需进程演算(Process Algebra for Demand and Supply, PADS)是由Philippou等提出的一种用于分层调度分析的形式化模型.在PADS模型中,用任务进程描述实时任务,实时任务一个时间单元的执行表示成它所需的带有优先级的资源的集合(如：{(CPU,3)});同时,使用供应进程来模拟资源供应方,资源供应方单位时间的执行表示为它提供的无优先级资源的集合(如：{CPU})；任务的可调度性通过任务进程的资源需求集与供应进程的资源供应集的满足关系来描述.目前,PADS模型下的调度理论包括：任务可调度的判定条件(如：供应模拟关系),调度的组合性,以及任务关于可调度性的层次性.对于这些理论成果,形式化分析、验证CPS系统中的调度问题还是个挑战.本文基于PADS模型对分层调度分析的形式化理论基础展开了系统的研究.首先,我们研究了PADS模型中的可调度理论；得到了PADS操作语义的若干性质和供应模拟关系关于算子“：”和算子“+”的组合性质；基于这些性质,通过一种分解-合成的方式为供应模拟关系建立了一个证明系统,并证明了它关于供应模拟关系的语义是可靠和完备的.任务关于可调度性的层次关系方面,我们扩展了原有的需求关系,得到了一种包含更多的调度性具有蕴含关系的任务序对的局部多需求关系,证明了：对于具有局部多需求关系的两个任务,其中一个任务的可调度性可以由另一个任务的可调度性得到,并且为推导任务之间是否具有局部多需求关系提供了一个推理系统,同时获得了该推理系统的可靠性证明和完备性证明.其次,我们在PADS模型中建立了部分可调度理论.任务可调度,要求任务的每条可执行途径上的资源需求都被供应进程满足.为了描述和分析任务中部分可执行途径上的资源需求被供应进程满足的情况,我们提出部分模拟供应关系,并定义任务的部分可调度性.关于部分模拟供应关系,我们讨论了它的性质,得到了：供应模拟关系是一个部分模拟供应关系,并为部分模拟关系的推理建立了一个证明系统,证明了它关于部分供应模拟关系的语义定义是可靠的和完备的.此外,我们提出了一个全函数式多需求关系,来描述任务关于部分可调度性的层次；证明了：对于具有全函数式多需求关系的两个任务进程,其中一个任务的部分可调度性可以由另一个任务的部分可调度性推出；并且针对任务关于部分可调度性的层次关系,建立了一个可靠且完备的推理系统,以帮助推导任务之间的全函数式多需求关系.最后,我们为PADS模型建立了进程等价理论,包括供应进程的迹等价关系和任务进程的互模拟关系.建立进程等价理论,是为了描述和刻画供应进程的资源供应行为以及任务进程的资源需求行为.我们以函数的方式定义了供应进程的迹,得到了供应进程的若干性质,其中一条性质是：供应进程的迹正好是它的所有转换序列中资源供应集序列的集合；并给出了迹等价关系的一个证明系统,证明了它关于迹等价关系的语义是可靠的和完备的.关于任务进程的互模拟关系,我们从任务进程的操作语义角度来进行定义；讨论了互模拟关系的一些性质,得到了：任务进程互模拟于一个不含算子“‖”的任务进程；并且建立了一个推理互模拟关系的可靠且完备的证明系统.此外,我们探讨了进程等价理论与可调度理论、部分可调度理论的联系,证明了：在可调度性的意义下,迹等价的供应进程所调度的任务相同；互模拟的任务进程具有相同的可调度性和相同的部分可调度性.