在现代公共交通体系中，轨道交通系统具有不可替代的突出地位。目前，我国的轨道交通正处在一个史无前例的大发展时期，人们对它有着很高的期望和要求。如何实现列车安全、快速、高效地运行，是摆在相关科研人员面前的一个突出问题。列车运行控制系统作为轨道交通系统的神经中枢，担当着保障行车安全和提高列车运行效率的重任。随着计算机技术在列车运行控制系统中的应用，安全问题显得越发的重要和复杂，传统的安全系统设计、分析和测试方法难以满足以计算机技术为基础的安全系统的需要。近年来，基于离散数学和形式逻辑理论的形式化方法发展迅速，为解决安全计算机系统设计开发的正确性问题提供了一条可能的途径。 论文针对轨道交通列车运行控制系统的特点，研究安全系统设计的理论和方法，尝试采用形式化方法进行系统安全设计和验证。论文主要以列车运行控制系统为研究对象，选择自动机模型和模型检验方法分别作为系统形式化建模和验证的方法，提出时间自动机网络模型和相应的模型检验算法，进而给出形式化设计验证方法ForTAN(Formal Design and Verification Methods based on Timed Automata Network)，最后以大连快轨3号线ATP车载设备为对象进行相关设计和验证，取得了不错的效果。这些成果这对于提高国内轨道交通列车运行控制系统的安全性设计水平，掌握系统关键技术，推动列车运行控制系统国产化具有重要的理论价值和实践意义。 论文主要的创新点有以下几个方面： (1) 针对轨道交通列车运行控制系统的特点，在有限自动机模型的基础上提出时间自动机网络模型，并且给出模型的形式化定义和相关特性，提出时间自动机网络模型的形式化描述语言TAN语言。和经典自动机模型相比，时间自动机网络模型有以下优点：①通过时间自动机网络模型，部分解决了经典自动机状态复杂性问题，使得建模过程变得较为简便，有助于进行系统的形式化设计和验证；②通过在组件自动机内部和组件自动机之间加入时间约束集，可以对系统的实时性进行描述；③通过描述组件自动机之间的动作集，可以描述系统的并发行为；④通过连续变量区域化方法有效的压缩了系统的状态数，解决了经典自动机理论不能描述连续变量的缺陷。 (2) 提出时间自动机网络模型的模型检验方法和步骤，主要的创新之处在于：①提出组件自动机(一种时间自动机)转换为带有时钟状态的有限自动机进行模型检验的思想；②基于DBM数据结构，提出计算时钟状态和状态迁移时间约束的