嵌入式实时系统是特定的计算机应用，它不仅必须满足各种逻辑关系，还必须满足指定的时间限制。除了高的可靠性和正确性要求，嵌入式实时系统大多都是异质的，特定的，设计具有这些特点的复杂系统是一个非常困难的任务。　　 形式的校验是确保设计正确性的一种可行的方法，通过对形式模型的有效化、校验，可以发现许多潜在的设计问题。因此，设计复杂的嵌入式实时系统时，在决定将系统分解成硬件和软件组件之前，形式的建模是非常必要的。　　 Petri网越来越多地用于嵌入式实时系统的建模，评估和分析。到目前为止，大多数使用Petri网建模嵌入式实时系统的方法主要关心系统功能的高级描述，经常忽视时间性质，例如调度，然而任务调度对于保证嵌入式实时系统的正确性起着关键的作用。现有的各种Petri网模型在建模调度时还有许多不足，为此，提出了一种扩展的时间Petrf网模型RBTPN。RBTPN将处理器资源和通信资源附着到变迁上，不仅可以直观地建模单个处理器上固定优先级的抢先式调度，而且可以应用到以下的分布式嵌入式实时系统：在处理器上实行固定优先级的可抢先式调度，而处理器之间的通信采用固定优先级的不可抢先调度。　　 详细地分析了RBTPN的语义和基本模型后，为了建立RBTPN模型的可达图，考虑变迁可抢先的特点，建立了两个重要的规则：1.确定在某个状态类下，可行的输出变迁。2.计算输出变迁的状态类。　　 在分布式嵌入式实时系统中，常采用多速率任务图来表示全部系统任务。在建模RBTPN模型之前，需要设置每个变迁所占有的资源和优先级。为此，提出了一种适用于分布式嵌入式实时系统的静态调度算法：基于裕度的调度算法，以便得到多速率任务图中所有任务的优先级和所占用的资源。该算法引入超周期的概念，将适用于单速率任务图的blevel算法进行扩展，从而可以处理周期不同，释放时间不同的多速率任务图。　　 为了检验调度算法的正确性，可以使用RBTPN模型进行调度分析，由于常规的的调度分析算法无法直接应用于分布式嵌入式实时系统，所以提出了两种新的调度分析的算法，解决了现有算法在多处理器系统中进行调度分析时存在的不足。在此基础上，改进了可达图的构造方法，将相对于各自状态类的触发域改为相对于初始状态类的触发域，从而可以更容易地计算调度序列的执行时间。分析了新状态类的性质之后，定义了调度序列的合并和分解，进一步建立了调度序列的触发域，然后进行化简，消除冗余的限制，得到最简的调度序列时间限制，从而可以分析调度序列的时间性质。