摘要：基于通信的列车控制(Communication Based Train Control，CBTC)系统是目前城市轨道交通列车运行控制系统的首选。CBTC子系统之间有大量的数据交互,数据作为设备、线路、列车状态等信息的载体,是CBTC系统的重要组成部分,其准确性和可靠性是实现列车安全高效运行的基础。随着系统功能的增强和系统复杂性的提高,数据量也有了显著的增加,因此,对数据的准确性和可靠性要求更高。基于以上需求,本文针对CBTC系统数据的特点,按照数据分析,规则提取,模型验证的路线,采用时间自动机对实际数据进行验证,确定了该方法的可用性和可行性。论文的研究内容主要包括以下几个方面：(1)论文从数据的建立、设计、使用与执行等数据开发生命周期的各个环节,对CBTC系统所需的线路网络数据、基础设备数据以及功能性数据进行分析和深入研究,得到CBTC数据验证的策略。分析CBTC系统架构和工程数据表现形式对系统数据构建的影响,进而分析CBTC系统数据组织方式,在此基础上得出CBTC系统数据所固有的特征。(2)论文在分析CBTC系统数据的基础上,对系统数据的关联关系和约束规则进行了总结。基于系统的数据需求以及当前工程数据的表现形式,围绕数据的性质和特点,从属性域值、关联关系和拓扑关系角度建立了CBTC数据规则库。(3)论文选取时间自动机理论和模型验证工具UPPAAL,分别对规则验证体系进行建模,形成一种数据的自动化验证机制,主要分为两步,一是将数据抽象为状态模型,二是将规则以数学或逻辑语言描述,给出了针对CBTC系统数据进行验证的评价准则。(4)论文基于规则的验证方法,采用北京地铁亦庄线中一个设备集中站的数据,并结合VOBC子系统功能,从数据本身和查询函数两个角度,对数据进行验证。结果表明,基于规则的CBTC系统数据分析与验证方法具有一定的适应性和可行性。