基于Agent的形式化理论研究是近年来形式化理论研究的前沿核心技术之一。列车控制系统是现今分布式实时监控系统中发展迅猛的应用之一。将Agent理论应用到列车控制系统的形式化研究当中是一次大胆的尝试。Event-B是一种处在发展前沿的形式化建模仿真语言，Rodin是它的建模仿真平台。Event-B通过对模型中Machine的逐层精化，对其中事件的不变式进行计算模拟，可以达到真实反映实际系统动态行为的效果；通过对模型中Context的逐步扩展，可以使模拟出来的环境更接近实际系统的环境；同时，Event-B具备了一般形式化理论所具有的完善的数学理论体系，能够用数学的方法来表述和计算系统运行过程中的各种状态，能够检验系统的逻辑正确性和完备性，对于系统的形式化建模仿真能起到有益的作用。智能Agent既要能完成自身的局部问题求解，又要能够通过协作求解全局问题，Agent之间相互协作产生不同的行为，从而才能适应不断变化的环境。每个Agent根据当前的状态和感知的环境信息及数据做出决策，决定自己的行为，同时，在多个Agent之间通过协作来解决当前的全局问题，完成共同的任务。智能Agent必须要具备自主执行简单任务的能力，多Agent系统则是要提供一种软件环境，在所提供的环境下，多个Agent之间通过协商、协调和谈判来实现协同作业，从而完成共同的任务，实现一个特定的应用目标，许多实时系统的实现都得益于Agent具有的灵活性和反应特性。论文首先描述了建模的相关概念与方法，介绍了Event-B的概念及基本知识，并介绍了智能Agent理论的基本原理，然后描述了Event-B语言在其Rodin平台下进行仿真建模的基本原理及模型。利用Event-B语言和智能Agent理论对列车控制系统当中列车注册与启动过程中车载设备与地面设施的通信交互问题进行形式化建模仿真研究，分析我国CTCS-4级列车控制系统中对列车注册与启动过程中车载设备与地面设施的通信交互过程设计的合理性和逻辑正确性。另外，还利用Event-B语言和智能Agent理论对列车控制系统当中车地通信故障恢复过程进行形式化建模仿真研究。然后利用Rodin平台分别对上述模型进行建模仿真，结合Event-B建模逐层精化的特点，针对性地提出问题与改进方法，证明系统的逻辑正确性。