基于通信的列车自动控制系统(Communication Based Train Control System,CBTC)是典型的由数据驱动的安全苛求系统,其子系统和各个单元集成来实现系统的功能都需依赖配置数据,所以CBTC系统的安全性和系统数据的质量密不可分。如何确保数据的质量,以形式化方法可以通过数学描述对系统的组成及其特点有精准详细的表达,而且可通过形式化建模的方法对系统特性进行建模验证;基于数据约束规则开发的数据验证系统能准确定位到某个数据的具体错误。本文采用建模验证和系统运行验证相结合的方法,对CBTC系统数据进行验证分析和检查,方便修改错误以提高数据质量。首先,论文分析了CBTC系统的组成成分和其系统的数据特点,基于此,对数据验证方法进行了调研,最终选择了基于时间自动机的模型验证和基于数据约束规则开发验证系统验证相结合的方法,既可以通过数学语言详细描述数据间的约束关系,也可以通过系统运行结果精准定位到错误数据。其次,在对CBTC系统特点、数据验证方案的设计以及相关理论知识和技术的了解下,对CBTC系统数据进行设计,从数据开发过程和数据描述的角度对数据进行分析。根据分析出的数据的特性,将数据关系分为值域关系、关联关系和网络拓扑关系三大类,并依据分类标准对数据约束规则进行归纳总结。然后,在归纳出的数据约束规则的基础上,进行数据验证的模型设计。根据规则将数据实体及其的属性时间自动机模型,通过状态的迁移描述数据关系。再基于归纳出的数据约束规则,从三类数据关系对大兴机场线的线路数据进行了建模和验证。最后,根据先前设计建立的数据约束规则的集合,对规则进行代码开发,数据约束集合转换为数据规则脚本库,数据验证系统调用规则脚本对输入的线路数据进行验证。从建模验证和系统验证两方面对数据的正确性进行检测,结果表明,该方案能有效准确的发现数据的缺陷。