摘要：安全计算机平台是轨道交通信号控制系统的核心基础安全设备,通过测试来检验安全计算机平台是否能实现设计的安全功能是至关重要的。传统的软件测试方法存在诸多问题,需要找到更为有效的,全面的测试方法。本文引入了基于模型检验的测试的概念,即用形式化的规范语言描述系统功能需求,再利用时态逻辑公式描述系统的性质并取反,以诱使模型检验工具输出不满足这一性质的序列形式的反例,那么这个反例就是满足系统性质的一段测试序列。基于这种形式化方法产生的测试序列是模型检验工具根据自身的算法生成,很大程度上避免了人为失误,并且提高了测试的效率及测试序列的完备性。首先,给出了基于模型检验的测试序列生成及优化方法。在描述符号模型检验原理和CTL(计算树逻辑,Computation Tree Logic)覆盖标准的基础上,通过分析测试序列的覆盖范围,证明了测试序列的覆盖完整性。通过分析生成测试序列的有限计算树,提出了测试序列的优化算法,并给出了其高效性证明。其次,生成和优化了安全计算机平台测试序列。在描述安全计算机平台结构、应用处理机和热备管理单元功能的基础上,根据有限状态机与SMV(符号模型检验,Symbolic Model Verifying)语言的转换规则,对安全计算机平台模型进行了形式化描述。进而通过模型检验工具NuSMV和构建的安全计算机平台测试覆盖标准,得出了应用处理机和热备管理单元的测试序列并给出了上述两种测试序列的优化结果。最后,搭建了安全计算机平台自动测试系统。完成了测试上位机、模拟应用处理机与热备管理单元的软件设计,实现了测试序列的提取与测试记录的保存。给出了自动测试系统对模拟应用处理机及热备管理单元的测试结果,证明了本文所提出的基于模型检验的测试序列生成及优化方法在安全计算机平台测试中应用的可行性。