模型检测是一种验证软硬件系统、多智能体系统、通信协议和嵌入式系统等的重要形式化方法。它将待验证系统建模为有限状态机,如Kripke结构、状态-迁移系统或自动机等,将系统期望的性质描述为时序逻辑公式；然后,自动化穷举搜索系统行为以确定待验证系统是否满足期望的性质。然而,现有模型检测方法大多基于显式状态空间描述和操作,即便使用动态状态空间构建和偏序规约等优化技术,可验证系统的规模仍然十分有限。在实际设计中系统模型的大小往往随着并发组件的数目呈现指数级增长,这一问题构成了将模型检测技术应用于实际设计的主要瓶颈。此外,模型检测的形式化规范语言(如计算树逻辑和线性时序逻辑等)的表达能力不足,描述顺序、并发和循环等性质较为困难,或者根本无法描述这些性质。因此,本文研究了命题投影时序逻辑的符号模型检测技术及其应用。命题投影时序逻辑(Propositional Projection Temporal Logic, PPTL)是对命题区间时序逻辑(Propositional Interval Temporal Logic, PITL)的扩展。它引入了新的时序操作符且被证明具有完全正则表达能力,能够方便的描述顺序、并行、选择、时间敏感和周期性等多种并发的系统性质。符号模型检测是一种应对显式状态模型检测中容易出现的状态空间爆炸问题的有效方法。它将待验证系统模型和系统期望的性质描述为布尔方程,然后通过基于规约有序二叉决策图的搜索算法查找系统模型中满足期望性质的状态集合。基于PPTL和符号模型检测方法的优点,提出了一个使用符号模型检测方法验证PPTL规范的统一框架。在该框架中,将待验证系统建模为Kripke结构M= (S,I,R,L),其中S表示有限状态集合,I表示初始状态集合,R(?)S×S表示集合S上的状态迁移关系,标记函数L用每个状态下成立的原子命题标记该状态；将系统期望的性质描述为PPTL公式φ。然后,将期望性质的否定形式,φ转化为它对应的范式。由于范式是构建标记范式图(Labeled Normal Form Graph, LNFG)的基础,且LNFG包含了目标公式所有可能的模型。因此,可以求得状态集合Sat((?)φ),使得对于该集合中的任意状态s,s包含于S且公式(?)φ在模型M中任何以s开头的路径上成立。通过这种方式可以将检查系统模型M是否满足期望性质φ的问题等价为检查初始状态集合I中满足(?)φ的子集Sat((?)φ)∩I是否为空的问题。事实上,通过进一步分析发现PPTL符号模型检测方法的时间杂度为O((log|V(φ)|)×|V(φ)|×(|R|+|S|)),其中|V(φ)|为公式φ的LNFG中顶点的数目,而|R|+|S|表示模型M的大小。此外,通过验证实例说明了PPTL的符号模型检测方法的可行性。基于给出的PPTL符号模型检测方法,本文研究了实时与嵌入式计算系统的形式化验证方法。以单调速率调度算法和延迟单调速率调度算法为例,验证了上述算法对任务集可调度性的充要条件。将任务集在单调速率调度算法和延迟单调速率调度算法调度下的行为建模为Kripke结构,将调度算法的可调度性描述为PPTL公式,然后调用PPTL符号模型检测方法对任务集在单调速率和延迟单调速率调度算法下的可调度性分别进行描述和验证。近几年来,基于线性时序逻辑和分支时序逻辑的符号模型检测方法是当前形式化验证领域最为活跃的研究课题之一,并实现了相应的符号模型检测工具,如SMV、NuSMV和NuSMV2等。但是,上述工具均受制于形式化规范语言的表达能力,无法完整描述顺序、并行、选择、时间敏感和周期性等性质。此外,上述符号模型检测工具均不支持以PPTL公式描述的规范。因此,本文在NuSMV工具中实现了PPTL的符号模型检测方法以支持对PPTL公式的验证。基于上述PPTL符号模型检测工具,本文研究了Verilog硬件描述语言程序的形式化操作语义和模型检测方法,并以Gigamax缓存一致性协议、交替位协议和PCI总线协议的验证为例解释PPTL符号模型检测工具是如何工作的。