高速铁路列车运行控制系统(简称：列控系统)融入了先进的计算机、通信以及控制技术,极大地提升了系统的效率和安全性。由于系统的硬件集成度不断提高,大量软件参与系统控制,使得系统特性也呈现出结构分布、实时性强、响应快速等多样化的趋势,系统特性的验证也愈加困难,因此需要找到一条更为有效、全面的方法实现列控系统的特性验证,进一步提升系统的性能或完善系统功能。基于严格数学定义的形式化方法,由于其能够精确、清晰地描述系统结构和相关特性,同时能够验证系统的相关特性,近年来在列控系统领域得到迅速发展,并且已经成为描述和验证高速铁路列控系统特性的一种重要方法。论文对列控系统的形式化建模、描述以及验证方法的应用展开了综述。分析了RAISE (Rigorous Approach to Industrial Software Engineering,工业软件工程的严格方法)形式化方法在列控系统中建模与验证的优势,并在此基础上,首次将Timed RAISE(时间化RAISE)引入列控系统验证领域。论文研究了基于域+Timed RAISE的高速铁路列控系统的建模和描述方法。结合高速铁路列控系统的实际特点以及复杂性,提出了一种域方法作为系统描述的切入。域方法的主要思想是将系统划分为规模较小的域模型,根据域的验证结果以及域之间的分解与组合关系,能够最终实现大系统的特性验证。论文详细给出了域的元组、域的组合分解以及域特性的组合分解等相关定义和定理,这些定义与定理也是域方法理论体系的关键组成部分。为实现对域方法的更好说明,对典型的高速铁路列控系统—CTCS-3 (China Train Control System level 3)级列控系统进行了实际的域的划分、域模型的建立、域特性的分析、域特性的组合分解以及子域的划分,实现了对域方法理论体系的有力支撑。论文研究了基于域+Timed RAISE的高速铁路列控系统的验证方法。对高速铁路列控系统常见的运营场景描述相关特性、系统功能以及系统性能等三类重要的域特性进行了详细分析,并给出了三类域特性中的场景交互一致性、安全功能以及实时性的定义和数学描述,并作为系统特性验证的重要依据。论文实现了域模型与Timed RAISE结合,给出了域模型转换为TRSL (Timed RAISE Specification Language)的具体规则,同时也给出了在系统TRSL描述的证明过程中相应的推理规则和证明方法。论文对基于域+Timed RAISE的描述和验证方法的具体应用进行了分析和举例。通过对RBC (Radio Block Center,无线闭塞中心)切换场景的交互一致性验证、等级转换(CTCS-2级至CTCS-3级)场景的实时性验证以及两车区间追踪案例中的安全功能进行了实际的域(子域)的划分、系统模型建立、Timed RAISE具体描述以及验证过程。仅为说明基于域+Timed RAISE方法的正确性,将各验证案例都进行了相应的简化和假设。最终给出了结果：列车通过RBC边界的条件下,车载设备与两个RBC的共同交互并不会带来场景交互一致性错误,即场景中各设备和子系统的交互流程是一致的；列车在等级转换(CTCS-2级至CTCS-3级)场景中,即使GSM-R (GSM for Railway)网络的通信随机延迟给场景的实时性带来了巨大的挑战,但依然能够满足场景的实时性要求；在两车追踪案例中,在给定前车以及外界的边界条件后,CTCS-3级列控系统能够在地面设备、车载设备以及GSM-R无线网络的共同作用下实现列车的安全运行。