列控系统需求文档结构的日益复杂,使得传统的文档测试方法在问题发现和测试效率方面逐渐难以满足要求。模型检测是一种用于对有穷并发系统进行正确性检验的形式化验证技术,它是提高系统可靠性的有效手段。本文针对传统的需求文档测试方法存在的不足,将模型检测与软件测试相结合,在对文档进行形式化建模验证的基础上,利用结果得到的反例生成文档测试项,提高了文档测试的自动化水平。状态迁移矩阵(State Transition Matrix)的规模会随着系统复杂度的提高呈指数级增长。针对这个问题,本文将分层结构引入状态迁移矩阵,使其具有更强的表达能力,以便更加有效的对现实中复杂的软硬件系统进行建模。首先,对列车制动控制系统需求文档进行形式化建模,其中分别对紧急制动和常用制动两个主要模块进行了层次化建模,以有效缓解随状态和事件数增加而造成的状态空间爆炸问题。基于扩展的建模方法,提出系统建模后的符号化编码和性质描述规则,并基于有界模型检测技术(Bound Model Checking,BMC)进行规范验证。通过在实际项目中对复杂软件文档的建模测试证明了该方法的可靠性。待验证性质的LTL公式规模是影响BMC转换公式规模的关键因素,本文首先利用LTL公式的等价性对性质公式进行简化,其次依据LTL公式向自动机的转换方法进行状态压缩,同时利用自动机中状态的等价性及可达性,再次压缩自动机规模,以达到缓解空间爆炸问题的目的。在此基础上,利用Garakabu II求解器对模型和属性进行形式化验证,将模型检测得到的反例作为测试需求文档的用例,以有效减少文档测试项的设计工作量。