在铁路信号系统中,联锁系统是不可缺少的核心技术装备,它通过技术方法实现车站管辖范围内的信号机、道岔和进路的制约关系,保证了站内行车安全,提高了铁路运输效率。近年来随着通信技术、控制技术和微电子技术的发展,提出了一种新型的联锁制式——分散控制联锁系统。分散控制联锁系统改变了传统集中控制的联锁方式,利用独立全电子模块与现场信号设备一对一采集或驱动,再通过电子模块间相互通信协作完成联锁逻辑运算,分散了联锁主机的联锁功能。这种系统的通信和时间参量非常重要,必须保证系统的安全运行。目前保证联锁系统正确性和安全性的方法有模拟、仿真和反复测试,但通过这些实验方法对系统进行查错所能涵盖的系统行为有限,很难找出系统所有潜在的错误。而采用形式化方法对分散控制联锁系统行为进行建模,可以减少联锁系统设计故障,在一定程度上解决该问题。本文首先根据分散控制联锁系统功能特点和计算机联锁技术标准,分析设计信号电子模块、道岔电子模块和轨道电子模块的进路控制工作流程,以此为依据得到系统通信架构和各电子模块的具体通信过程。其次再结合时间自动机理论建立始端信号电子模块的时间自动模型、敌对信号电子模块的时间自动机模型、道岔电子模块的时间自动机模型和轨道区段电子模块的时间自动机模型。最后利用基于时间自动机理论的UPPAAL验证工具建立系统进路控制过程的时间自动机网络模型；使用模拟器进行随机实验,得到系统进路控制过程的仿真时序图,分析系统通信过程和状态变化；在验证器中,用BNF语法提取系统待验证的性质,验证分散控制联锁系统的功能特性、时间特性和安全性。