列车自动防护(ATP)系统是列车运行控制系统的核心子系统,系统的安全性和可靠性直接关系到列车的运行安全。ATP系统作为典型的、复杂的安全苛求实时系统,系统功能复杂,系统内部相互通信频繁,对实时性有很高的要求。系统既要求逻辑运算结果是正确的,又要求必须在规定的时间限制内产生结果。如何保证开发的ATP系统功能与系统需求规范的一致性,进而保证系统的正确性和安全性成为研究人员亟待解决的问题。形式化方法是以严格的数学理论为基础,可以对系统需求规范进行准确的描述,避免了自然语言的随意生,能够很好地解决上述问题。本文在对形式化方法进行分析和比较的基础上,选择时间自动机理论描述实时并发系统功能流程。以ATP系统为例对时间自动机进行详细的分析,研究了构建系统时间自动机网络模型的方法,并对UPPAAL这种行为模型验证工具进行了详细的研究。论文以轨道交通列车自动防护系统为研究对象,对系统的功能进行详细的分析,着重研究了系统的速度监督与超速防护功能以及同步功能。针对系统功能需求,采用UPPAAL模型验证工具对超速防护和同步功能流程进行形式化建模,并对模型的安全性和受限活性进行验证。通过验证,证明了模型功能与系统需求的一致性,表明使用时间自动机对ATP系统流程进行建模和分析,是保障ATP系统功能正确性和安全性非常重要的途径。论文用VC6.0软件工具对车载ATP速度防护模型进行了设计与仿真,实现了车载ATP的速度监督与超速防护功能。