计算机软硬件系统日益复杂,在很多系统中,测试、模拟等传统的验证方法已不能保证其正确性和可靠性。模型检测技术产生于上世纪80年代,由美国的Clarke和Emerson,法国的Quielle和Sifakis分别独立提出。在该形式化验证方法中,系统性质用命题时态逻辑公式表示,有限状态反应系统(硬件电路、通讯协议)用状态转换系统描述,有效的查询过程检测模型,判断模型是否满足系统性质。然而,随着系统规模的增大,状态数呈指数上升的状况和显式模型检测有限的处理能力之间存在难以克服的矛盾,即状态爆炸。1986年,Bryant将传统的二值判定图BDD技术加以改进,使之成为布尔函数的规范表示方法。之后McMillan将这种技术应用于模型检测中,基于BDD的模型检测称为符号模型检测。符号模型检测的主要特点是用BDD隐式地表示有限状态反应系统的状态集合和状态转换集合,空间爆炸问题被有效缓解。本研究实现了一个基本的符号模型检测器CTLMC。该模型检测器直接采用布尔函数作为系统模型的描述语言,用来描述模型的初始状态集合和系统状态转换关系;采用CTL时态逻辑作为系统性质的描述语言,用来描述系统应该满足的需求(性质);采用CTL符号模型检测算法计算模型是否满足性质。此外,在实现CTLMC过程中发现一种基于BDD的SMC中PRE(?)操作的改进算法,该算法处理PRE(?)步骤3(嵌套布尔存在量化)的方法是,一次遍历“删除”所有被量化变量的节点,产生表示布尔函数与嵌套存在量化结果等价的不确定排序二值判定图,然后把不确定排序二值判定图转换成OBDD。实验表明该算法能有效缩短计算时间,减少中间节点所需空间。