计算机软硬件系统日益复杂,其正确性和可靠性已成为计算机领域中研究的热点,在诸多方法和理论中,模型检测以其简洁明了和自动化程度高而倍受关注。模型检测的关键问题是状态爆炸问题,具体来说就是如何使用精简方式描述系统,避免因为模型复杂而引起状态爆炸。模型检测技术的成功应用必须以有效验证工具为基础,NuSMV作为一种有效的分析验证并发系统逻辑一致性的模型检测工具得到了越来越广泛的应用。本文在阐述模型检测形式化分析机理及时态逻辑性质的基础上,详细分析了NuSMV作为一个模型检测器在PCI协议总线上的应用。通过详细分析PCI总线协议规约的要求,基于NuSMV对PCI总线协议的总线命令和总线信号及动作进行了建模,包括总线信号和命令的建模,主从设备读／写transactions的建模及设备调度策略的建模。应用NuSMV进行了具体的实现并检测了其属性对规约的要求,结果表明：如果NuSMV检测的结果是FALSE,则说明属性不满足,且NuSMV可以给出其反例来详细说明违反属性的步骤从而让检测者一目了然,检测结果与PCI总线协议的实际逻辑是一致的,表明我们对PCI总线协议的建模是可靠的。文章描述的检测方法具有一定的普遍性,可用于对正确性和可靠性要求比较高的系统。