中国列车运行控制系统(CTCS)是一个典型的复杂巨系统，是分布式智能系统的一个具体应用。多Agent系统(MAS)的形式化建模与验证是近些年来形式化理论研究的前沿技术之一。因此本文创新地将MAS理论应用到列车控制系统，为了保证该系统的正常运行并达到相应的安全技术指标，本文对列车运行控制系统的车地通信抽象为MAS并进行形式化研究。本文首先进行了形式化建模的相关概念及方法介绍，并介绍了通信顺序进程的定义概念及基本知识，随后介绍了多Agent理论(MAS)的相关理论，然后描述了通信顺序进程(CSP)语言在其模型验证器FDR2平台下进行建模验证的基本原理及相关的模型。其次本文利用CSP语言和多智能体理论，对列车运行控制系统场景中列车RBC切换场景中车地通信交互的问题进行形式化建模仿真研究，分析CTCS-4级列车运行控制系统中对RBC切换过程中车地通信交互过程中协议设计的完整性和安全性，并对注入故障时通信的时效性进行仿真分析。另外，还利用CSP语言和智能Agent理论对列车控制系统当中车地通信过程进行形式化建模仿真研究。然后利用平台分别对上述模型进行建模仿真，结合CSP的特点，建立相关的协议模型并证明系统协议的安全性。并通过注入故障的注册协议模型进行形式化建模并利用TIMENET4.0进行定量分析，得出随着列车数量增加以及信息发送周期变化对于通信时延的影响。对于CTCS-4级系统具有一定的指导意义。论文的最终研究结果表明，论文提出使用MAS和CSP相结合的研究方法具有一定的适用性，能对MAS模型进行安全性检测并保证系统的安全苛求性要求。CSP语言具有很强的描述能力，为以后CTCS-4的规范制定及工程实施提供了理论参考依据。最后对本文所做的研究做了相对系统全面的总结，主要包括本文的相关结论和创新点，并对下一步要做的工作重点做出了展望。