当今,并发程序设计已成为计算机界关注的研究领域.众多学者利用Pteri网、时序逻辑等理论工具进行这一领域的研究.然而,这些理论模型都还存在着不足之处,该文旨入了时序Pteri网,以弥补上述理论模型的不足.首先,在介绍时序Pteri网的基本概念和相关性质的基础上,提出一个解决哲学家用餐问题的时序Pteri网模型,并形式化地验证了该模型能够满足互斥等问题要求,实现系统的公平调度,满足了无饥饿性.其次,利用时序Pteri网对Ada任务程序进行建模,构造了时序Ada网,反映了程序语句执行的公平性和原子性要求,从而有效地描述了Ada任务程序的物理结构和系统要求,同时,分析了该网性质,刻画其语言特性.基于网的同步合成运算,有效地降低了求解时序Ada网可达图的复杂性,并据此求解了网语言.在此基础上,给出了死锁、活锁等程序性质的语言判据.最后,借助时序Ada网的动态运行和时序逻辑公式演绎,验证程序的安全性质和活性性质,达到程序正确性证明的目的.