摘要：为了确保列车运行控制系统设计和开发的正确性，比较了仿真、测试和形式化3种能够验证系统设计正确性的方式。根据列车运行控制系统对安全的苛求性，提出了4个与系统安全相关的重要特性，即实时性、混成性、分布（并发）性、反应性，并分析了与这些特性相关的具体形式化方法。通过对每种形式化方法的数学基础和应用范围的分析和归类，给出了各种方法的优势和不足。分析结果表明：任何形式化方法的应用都具有一定的局限性，这是由模型检验和定理证明的本质所决定的；指出了新方法提出、既有方法拓展以及多方法集成将是列车运行控制系统的形式化领域的方向。

关键词：交通信息工程 形式化方法 列车运行控制系统 安全苛求系统 

单位：北京交通大学轨道交通控制与安全国家重点实验室; 北京100044; 铁道部科学技术司; 北京100844