基于通信的列车控制(Communication Based Train Control, CBTC)系统是保证列车运行安全、提高运输效率的安全苛求系统。CBTC各子系统依靠配置数据来定义系统的功能,数据作为系统核心组成部分,其正确性是CBTC系统安全连续运行的重要保证,如何保证数据的正确性,寻找一种有效的研究方法对整个CBTC系统具有非常重要的意义。基于严格数学定义的形式化方法不仅能精确、清晰地描述系统结构和相关特性,而且能对特性进行验证,本文采用形式化的方法对CBTC系统数据进行验证,以此来保证系统数据的正确性。首先,论文分析了CBTC系统结构组成与数据特点,根据安全苛求系统和CBTC系统的具体需求,结合时间自动机理论和模型分析验证工具UPPAAL,提出了基于UPPAAL的CBTC系统数据验证的方法,并设计了CBTC系统数据验证的具体建模方法和验证流程。然后,论文在前述理论基础和流程设计的基础上,按照CBTC系统数据的形式化验证机制,先后对CBTC系统的数据组成与描述方式进行了分析和深入研究。围绕CBTC系统数据的性质和特点,总结了CBTC系统所需的基础线路数据、轨旁设备数据以及区域功能数据,得到CBTC系统数据验证的策略,从值域关系、参照关系和逻辑关系三个角度建立了数据约束集合,并根据这些数据约束条件对CBTC系统数据验证体系进行建模,形成一种数据的自动化验证方法。先将系统数据抽象成带有状态的时间自动机模型,然后把数据约束条件以数学公式和逻辑语言的方式加以描述,并针对CBTC系统数据进行验证的结果进行分析。最后,论文针对北京地铁亦庄线的实际数据,运用时间自动机理论和模型验证工具UPPAAL,根据不同的系统数据和数据约束条件,通过分层递进的方式对数据进行了建模和形式化验证。结果表明,基于UPPAAL的CBTC系统数据验证方法具有一定的可行性和可用性。