有轨电车作为方便快捷的公共交通工具，其安全性直接关系到广大乘客的生命安全，为了保证其安全、高效运行，需要有安全可靠的控制系统作保障，有轨电车运行控制系统的主要功能包括道岔控制、安全防护、速度控制、自动驾驶等功能[1]。现代有轨电车运行控制系统已经从轨道电路、机车信号等设备的简单组合，逐渐向功能完善、层次分明、集运行控制及自动驾驶为一体的综合自动化系统方向发展，呈现出系统化、网络化、信息化、智能化及通信信号一体化的特点[1]。

随着计算机在列车运行控制系统中的广泛应用，硬件和软件规模不断扩大，使得计算机系统的复杂程度不断增加，系统的复杂性大大提高，从而使设计和开发计算机系统的难度也在增加，硬件方面，即使是最简单的计算机系统也包含数以万计的元器件和非常复杂的行为状态就软件而言，比较简单的软件程序也可能有数以千计的执行路径[2]。复杂的系统很难设计开发，寻找错误和安全隐患也比较困难，对于轨道交通列车运行控制系统这样的安全苛求系统来说，系统的任何故障都有可能造成重大的人身伤亡和财产损失，如何保证计算机系统设计开发的正确性和安全性成为人们亟待解决的问题[3]。

1.2 国内外研究现状

1.3 研究目的及意义

从有轨电车控制系统安全技术的发展看，计算机技术在有轨电车控制系统中的应用使得系统呈现出系统化、网络化、信息化、复杂化等特点，硬件和软件规模不断扩大，使得计算机系统的复杂程度不断增加，系统的复杂性大大提高，复杂的系统很难设计开发，寻找错误和安全隐患也比较困难，从而使得设计和开发计算机系统的难度也在增加[3]。为了适应国内轨道交通快速发展的趋势，提高列车运行控制系统的国产化水平，必须紧跟科学技术发展的潮流，研究适应于计算机技术的系统安全性设计方法，提高列车运行控制系统安全性设计水平[4]。

从形式化方法在轨道交通领域应用的情况看，在计算机系统从上层规范至最终实现的过程中，采用形式化语言对于系统需求进行描述，选用适当的形式化工具对于系统进行辅助设计和安全性验证，可以在很大程度上减少由系统开发人员造成的设计故障，提高系统的安全性[5]。论文根据有轨电车控制系统的特点，研究相应的形式化建模和模型验证方法，最大限度的避免系统的设计故障，提高系统的安全性，为我国轨道交通列车运行控制系统的自主研发提供理论和技术支持[3]。

1.4主要研究工作

第一章作为绪论，在阅读大量相关文献的基础上，对于有轨电车的发展和形式化方法在轨道交通领域的应用情况进行了综述和比较，指出研究有轨电车控制系统形式化设计验证方法的重要意义。

第二章针对有轨电车运行控制系统的特点，对有轨电车信号系统的物理模型进行了分析和比较，选择合适的物理模型。

第三章提出了自动机网络模型，给出了模型的形式化定义和相关特性，对形式化建模方法进行研究。

第四章在时间自动机网络模型基础上提出形式化设计验证方法，并对有轨电车控制系统进行形式化建模和验证。