毕业设计（论文）-基于UPPAAL的列控系统的仿真验证.doc

西 南 交 通 大 学 本 科 毕 业 设 计（论文）基于UPPAAL的C2/C3列控系统切换的仿真验证THE SIMULATION AND VERIFICATION OF C2/C3 CHINESE TRAIN CONTROL SYSTEM SWITCHING BASED ON UPPAAL 年 级 2010级 姓 名 学 号 20108150 专 业 通信工程（铁道信号） 指导老师 2014年6月承 诺 本人郑重承诺：所呈交的设计（论文）是本人在导师的指导下独立进行设计（研究）所取得的成果，除文中特别加以标注引用的内容外，本文不包含任何其他个人或集体已经发表或撰写的设计（研究）成果。对本设计（研究）做出贡献的个人和集体，均已在文中以明确方式表明。如被发现设计（论文）中存在抄袭、造假等学术不端行为，本人愿承担一切后果。 学生签名： 年 月 日第III页 西南交通大学本科毕业设计（论文） 院 系 计算机与通信工程系 专 业 通信工程（铁道信号） 年 级 2010级 姓 名 宋 菲 题 目 基于UPPAAL的C2/C3列控系统切换仿真验证 指导教师 评 语 指导教师 (签章)评 阅 人评 语 评 阅 人 (签章)成 绩 答辩委员会主任 (签章) 年 月 日 毕业设计（论文）任务书班 级 10信号4班 学生姓名 宋 菲 学 号 20108150 发题日期：2014年2月24日 完成日期：2014年6月5日题 目 基于UPPAAL的C2/C3列控系统切换仿真验证 1、本论文的目的、意义铁路在世界范围内都是快速发展的产业。随着铁路的快速发展，列车的运行速度大为提高，并且因为计算机技术和人工智能技术的飞速发展，以前人工手动的控制逐渐被淘汰，取代它的是智能的控制系统-列车运行控制系统。列车运行控制系统作为铁路运输的一个核心部分，其安全性尤为重要。本论文是基于UPPAAL的高速铁路列控系统的等级转换的建模和分析验证，为其软件设计提供指导和参考，可以消除部分系统设计之初时的逻辑矛盾、定义模糊、功能混乱等情况，这样保证列车运行控制系统的安全性和可靠性。 2、学生应完成的任务 明确列车运行控制系统相关概念、发展历史和背景等； 了解形式化方法的研究领域和发展现状； 分析列控系统的控制原理； 分析列控系统等级转换的过程； 运用UPPAAL软件对列控系统等级转换进行建模和分析验证 阅读相关资料，对论文进行了补充。 最终提交的资料有：毕业论文、外文翻译。 3、论文各部分内容及时间分配：（共 18 周）第一部分 查阅相关资料、检索文献 ( 1 周)第二部分 整理分析资料、构思论文提纲 ( 2 周)第三部分 建立列控系统等级转换分析模型 ( 4 周)第四部分 建立验证模型，撰写论文初稿 ( 6 周)第五部分 论文修改及编排完善 ( 2 周)论文评阅及答辩 ( 2 周)论文整改 ( 1 周)备 注：答辩前应向指导老师交毕业设计（论文）说明书（书面文档应不少于1万2千个汉字）和电子文档（含毕业设计（论文）说明书及应用软件） 指导教师： 年 月 日审 批 人： 年 月 日第V页 西南交通大学本科毕业设计（论文） 摘 要随着铁路产业的快速发展，列车的运行速度快速提高，但是铁路安全事故时有发生，为了既保证铁路的运行效率又保障人生财产安全，所以对铁路运输的安全性有极高的要求。CTCS是我国自主研发的列车运行控制系统，符合我国既有的铁路线路技术和规范，也符合我国的基本国情。CTCS一共分为五级（CTCS-0级CTCS-4级），其中CTCS-4级为将来的发展保留着，其他CTCS-0CTCS-3级能够满足不同的线路和速度的要求。列车在铁路上运行时，为了运行通顺并且设备出现故障后列车降级运行的需求，需要进行列控系统的等级转换。在列控系统等级转换的过程中，很可能因为应答器的信息未成功接收，数据丢失，速度没有达到允许值等原因，造成列控系统的等级转换不能够成功，因此需要通过对列控系统的转换过程进行建模和分析验证以保证列车运行的安全。形式化方法是一种验证分析实时系统的可行性和安全性的数学方法，利用形式化方法，是通过数学方法的形式对系统的软件和硬件的规定和约束进行定义和描述。形式化方法在很多领域已经得到成功的运用，比如信息安全学、航天事业、过程及控制和通信工程等等。现阶段，在铁路领域使用形式化方法也是很普遍的，在系统开发前期为了保证列控系统的安全性和正确性，普遍采用形式化方法对列控系统进行建模和仿真验证。本文采用基于时间自动机的UPPAAL软件对CTCS-2、CTCS-3等级转换过程进行建模和验证，验证等级转换过程的安全性和可靠性，并对现有技术规范提出了改进意见。关键词 铁路产业；安全性；列车运行控制系统；等级转换AbstractWith the rapid development of the railway industry,the rapid increase in the speed of the train ,but railroad accidents occur frequently, in order both to ensure the efficient operation of the railway and the protection of life and property , so the safety of rail transport have high demands . CTCS is our self-developed train operation control system , in line with our existing railway line technology and norms, but also in line with Chinas basic national conditions. CTCS total is divided into (CTCS-0 level CTCS-4 level) five , where class CTCS-4 retained for future development , other CTCS-0 CTCS-3 stage is capable to meet the different lines and speed requirements. In order to meet the needs of rail lines and interconnection equipment failure after downgrading the train running , the train during operation , the need for level conversion. Train Control System level in the process of conversion , probably because the transponder does not successfully receive the information , data loss, speed does not reach the allowable speed and other factors, led to the conversion level can not succeed , it needs through formal modeling of the train control system the conversion process modeling and analysis verification.Formal verification method is a mathematical method of analysis of the feasibility and safety of real-time systems , is in the form of mathematical methods for systems software and hardware requirements and constraints are defined and described . Formal methods have been successful in many areas of use , such as information security science, aerospace industry , process and control and communications engineering , and so on . At this stage, the use of formal methods in the field of railways are also very common in the early development of the system in order to guarantee the security and accuracy of train control system , widely used formal method for the train control system modeling and simulation.In this paper, proposed improvements based on time automata UPPAAL5 software CTCS-2, CTCS-3 level conversion process modeling and verification , validation level of security and reliability of the conversion process , and the existing technical specifications.Key words Railway ； safety； train operation control system； Level Conversion 西南交通大学本科毕业设计（论文）目录第1章 绪 论31.1研究背景及意义31.2研究现状41.2.1形式化方法在铁路系统领域的研究现状41.2.2时间自动机在铁路系统领域的研究现状51.3选题的目的和意义51.4论文研究的主要内容6第2章 形式化方法和UPPAAL的介绍72.1引言72.2形式化方法定义72.3形式化验证82.4时间自动机介绍和UPPAAL介绍92.4.1时间自动机92.4.2 UPPAAL的介绍9第3章 列控系统及其C2/C3等级转换流程分析123.1列控系统的介绍123.1.1 CTCS的基本功能123.2 列控系统基本原理123.2.1 CTCS的等级划分143.2.2 CTCS-2级列控系统工作原理153.2.3 CTCS-3级列控系统工作原理16第4章 C2/C3等级转换过程建模与验证174.1列控系统的等级转换过程174.1.1固定位置等级转换174.1.2设备故障情况下等级转换194.2 C2/C3等级转换过程分析与建模194.2.1 C2/C3等级转换过程分析和模型建立194.2.2 C2/C3等级转换流程形式化验证21 西南交通大学本科毕业设计（论文）结论和展望27致 谢28参考文献29第 27 页 西南交通大学本科毕业设计（论文）第1章 绪 论1.1研究背景及意义中国是世界上人口最多的国家之一，为了解决大规模人口的流动问题，需要大力发展高速铁路，这不仅是因为铁路具有巨大的运载能力，还因为铁路运输的安全性和可靠性也越来越高。随着我国铁路事业的快速发展，越来越多的高新技术都逐渐运用到铁路的大规模建设中，列车的运行速度也越来越高，列车运行间隔也越来越短，安全问题也越来越突出。当列车的速度达到200km/h时，通过1.2km的闭塞分区只用到22秒，这样就会导致司机频繁的瞭望信号，很之容易产生疲劳，司机很容易错误辨认信号。经过大量的试验后，专家认为只要列车速度超过200km/h时，依靠司机人为的辨别地面信号是不安全的。因此，完全的靠人工瞭望信号，人工驾驶列车已经不能完全保证行车安全了。装备了机车信号和自动停车装置的列车，也只能在一般运行速度运行条件下，才能够保证安全。但是如果按照这样，列车将无法实现速度的提高，因为不能防止超速行车和冒进信号现象。鉴于此种现象，铁路的发展需要列车运行控制系统（以下简称列控系统），来实现对列车间隔和速度的自动控制，进一步提高运输效率和确保行车安全11。列车控制系统以速度信号来代替色灯信号，将车载信号作为行车的凭证，具备了高速铁路行车所需要的安全性保障条件，而且车载信号设备能够直接控制列车减速和停车。列车运行控制系统简称列控系统，是铁道智能化的主要组成部分1。列控系统的基本原理是，根据列车与先行列车之间的距离和进路条件，计算出当前允许的运行速度并在列车内显示，列车必须按照该显示的允许速度，自动或人工驾驶列车运行。列控系统在国内和国外都得到了普遍运用。在国外，列控系统系统的发展比较快速，运用于各级速度，但是高速铁路的列控系统更具有代表性。目前，欧洲国家主要使用的列控系统有日本铁路ATC和数字ATC、欧洲ETCS、德国LZB80、法国U/T等。在国内，铁道部参照欧盟ETCS相关标准，结合我国现有的信号技术设备，自主研发了符合我国国情的列控系统（CTCS）。由于列车运行控制技术是高速铁路核心技术之一，关系着重大的人财的安危，因此列控系统对安全性的要求极高，所以及时的建立列车运行控制系统模型并且在实验室进行仿真验证具有积极深刻的意义。在系统软件的开发中，模拟仿真验证需要耗费大量的人力和物力，而且实验所能包括的系统行为是非常有限的，这样比较困难提前找出系统中隐藏的错误和疏漏。于是通过借用常用的数学工具，描述和模拟仿真验证列控系统已经成为一种笔记普遍的方法，并且这种方法可靠性比较高。形式化方法是近几年来常用的，一种严格检验系统可靠性的数学方法，它能够有效的检测出系统软件设计和开发的正确性和安全性。但是形式化检验方法又基于很多理论基础，其中时间自动机对于检验对时间严格约束的列控系统是最合适不过的，时间自动机是在位置和位置的转换上增加时间约束，这样形式化方法就能够有效描述实时性强的列控系统模型。时间自动机理论在铁路领域已经得到广泛的运用。1.2研究现状1.2.1形式化方法在铁路系统领域的研究现状 形式化方法是一种验证分析实时系统的可行性和安全性的数学方法，利用形式化方法，是通过数学方法的形式对系统的软件和硬件的规定和约束进行定义和描述。形式化方法在很多领域已经得到成功的运用，比如信息安全学、航天事业、过程及控制和通信工程等等。现阶段，在铁路领域使用形式化方法也是很普遍的，在系统开发前期为了保证列控系统的安全性和正确性，采用形式化方法对列控系统进行建模和仿真验证很有必要。形式化的方法解决了复杂系统在设计阶段所隐藏的问题，这样的做法就能极大的减少软件开发的风险。采用形式化的方法描述的系统是精确的，这样的系统不会存在概念上的模糊性、二义性和矛盾。它能够使用户明确自己本来含混的目的，发现和解决用户本身提出的问题的矛盾。这样所得出系统才是正确的，没有偏差。形式化方法的种类有很多，包括描述类、操作类和双重类。操作类是通过可执行模型来描述系统，主要存在的对象时状态和转移，通过静态分析和执行来验证，常见的有时间自动机和有限状态机。描述类具有高度的抽象性，是基于数学公式的基础上，通过代数和逻辑的方法描述系统的状态空间，比如Z。双重类兼具有操作类和描述类的特点，比如TROL。形式化方法分为形式化验证方法和形式化规范方法。形式化规范方法研究的主要对象是形式化规范，它是通过精确的语义来描述系统的功能，是系统设计的出发点，也是验证程序是否正确的重要依据。形式化验证是指严格的运用数学公式来验证产品和设计是否满足全部的规范化要求。在完成形式化规范以后就进行形式化验证，这样就能提前发现设计中的错误并改正。目前的形式化验证分为：模型检验和定理证明。模型检验适合有穷状态系统，优点是自动化和检验速度快，但是缺点是需要模型检验工具才能实现。定理证明是完全采用逻辑公式来证明和验证系统，其中的逻辑是有公理或规则演变的，其证明过程就是由这些公理来推导系统的性质。这种方法更适用于无限状态系统的情况。1.2.2时间自动机在铁路系统领域的研究现状时间自动机为列控系统这类实时系统提供了一种建模和分析验证的形式化方法，为确保系统的安全性和正确性，列控系统必须要满足很多方面的时间约束，执行时间，通信延迟和响应时间在列控系统的等级转换是必须进行明确的限制。 在模型中的状态转换时既可以检查时钟也可以将时钟清零。通过时间自动机，可以直观的观察到和时间有关的行为特征，并且反应了实时系统的控制行为，同时验证系统的性质时间自动机。自动机理论被时间自动机扩展了，为实时系统的建模和分析验证提供了解决方法。在计算机理论科学里，时间自动机理论已经成了研究的热门课题。从目前的专题文献中可以看出，时间自动机理论已经发展的比较成熟，并且运用很广泛，并且基于时间自动机理论的模型验证技术是目前主要的研究方向。时间自动机理论的不断发展带动了理论的验证工具也不断发展。现阶段形式化验证的工具有很多种比如Timed COSPAN、KRONOS、UPPAAL等等。目前在列控系统领域里，时间自动机理论已经发展成为分析列控系统的常用工具。1.3选题的目的和意义中国是世界上人口数最多的国家之一，为了解决大规模的人口流动问题，应该大力发展安全、快捷、经济、环保、可靠地高速铁路。中国铁路的客运告诉是实现现代化的一个重要方向，铁路运输的高速发展能够带动国内其他产业的快速发展，铁路运输是其他产业发展的决定性因素。近年来，高速铁路在世界范围内都是迅速发展的。我国的高速铁路的发展也紧紧跟随着世界的潮流。目前，我国已经自主研发了CTCS0-CTCS4级列控系统，其中CTCS3的运营速度已经达到了350km/h，由此可以看出我国的高速铁路控制系统已经达到世界先进水平。根据我国铁路网的规划，中国客运专线规划为“四纵四横”。“四纵”客运专线：北京上海：简称“京沪”。北京武汉长沙广州深圳：简称“京广”。北京沈阳哈尔滨（大连）：全长约1700km。杭州宁波福州深圳：简称“东南沿海铁路”。“四横”客运专线：徐州郑州兰州：全长约1400km。上海-杭州南昌长沙昆明：简称“沪昆”。青岛石家庄太原：全长约770km。上海南京合肥武汉重庆成都：全长约全长2078km。到2020年，全国铁路的运营里程应达10万千米，其中客运专线1.2万千米以上，车速目标值达200km/h及以上。鉴于我国正在大力发展铁路，所以对列控系统进行建模仿真和验证，以确保列控系统的安全可靠性，对铁路的发展无疑是重要的。1.4论文研究的主要内容本文研究的主要对象时基于UPPAAL的高速铁路等级转换流程的分析与建模。该论文采用形式化方法作为研究的理论基础和采用以时间自动机为基础的验证工具UPPAAL，来对高速铁路列控系统的等级转换过程进行建模、验证和分析。通过阅读和整理大量文献，对列控系统等级转换的过程进行了深入的研究，最后利用UPPAAL对等级转换过程进行时序仿真和验证分析，论文的组织如下：首先介绍了课题研究的对象和背景，介绍了列控系统在国内外的发展现状第一章介绍了形式化方法的理论基础-时间自动机理论，和时间自动机为理论基础的UPPAAL，以及UPPAAL作为列控系统等级转换建模和验证的工具2。第二章详细描述了列控系统的组成、功能和工作原理，并且详细介绍了列控系统等级转换的过程。第三章在第二章的基础上对列控系统进行了建证，并且采用UPPAAL对等级转换的功能性和安全性要求进行仿真验证，对仿真结果进行分析和提出修改意见。第2章 形式化方法和UPPAAL的介绍2.1引言形式化方法的定义是：“用于开发计算机系统的形式化方法是基于数学的用于描述系统性质的技术。这样的形式化方法提供了一个框架，人们可以在该框架中以系统的方式刻画、开发和验证系统12”。即形式化方法就是用严格的数学语言和精确的数学语义组成的。从广义上讲，形式化方法是系统设计过程中开发和验证的方法。从狭义上讲，形式化方法是对规格和验证的方法。随着计算机技术的高速发展，现代的软件系统越来越复杂，软件的生成越来越自动化，自动化的前提是形式化。其中软件规范说明书既是面对用户需求，也是系统的严格定义4。所以规格说明书相当重要，能够提高系统软件开发的效率。规格说明书必须精确，以保证软件系统的可靠性。需求规格说明书的使用者不单单是用户，还有系统分析人员、设计人员，检验测试人员等等。如果规格说明具有歧义性和概念模糊性，这将会导致人员不同的理解。为了克服上述缺点，必须采用形式化方法即严格的数学方法来描述软件的目的。形式化方法运用严格的数学符号和数学法则对软件的行为和结构进行推理和分析，有助于检验需求的一致性。2.2形式化方法定义形式化方法主要分为：形式化验证方法和形式化规格方法4。如图2-1，形式化方法示意图。图2-1 形式化方法示意图1.形式化规格（Formal Specification）方法，能够精确的描述软件的功能和性质，以及用户的需求。它具有严格的数学语法和语义，它描述的是“做什么”，而不是“怎么做”，帮助用户明确自己原本的目的和需求。系统特性包括：行为特性、性能特性、时间特性、内部结构等。它大概可以分为三大类：（1）具有可执行模型的操作类；（2）高度抽象的描述类；（3）两者特点兼具的双重类。2.形式化验证（Formal Verification）方法主要包括定理证明和模型检验。形式验证是指用严格数学方法，来推理验证产品或设计是否符合其全部或部分规范的过程。形式验证要求产品的规范和实现有严格的形式描述。主要有两种方法：（1）模型验证（Model checking），基于有限状态模型，构造一种算法建立根据设计的模型，确认模型是否满足规范说明。（2）定理验证（Theorem proving）包含多种数学逻辑公式，该逻辑是由公理推到出来的。其证明过程就是用公理和规则推导出被证明的软件的某种性质。另外，形式化方法根据表达能力分为四种：a. 基于逻辑方法：利用逻辑来描述系统的语气功能。b.模型方法（Model）方法：针对非功能性要求，不能很好的阐述并发性。c.过程代数（Calculus）方法：通过限制可观察间的通信来描述系统，具有并发性。d.代数（Algebra）方法：通过未定义状态联系不同的行为。2.3形式化验证前文提到了形式化验证主要分为两大类即模型检验与定理证明，本论文主要介绍在形式化验证中具有代表性的工具:1.模型检验工具：（1） 组合验证器：上世纪80年代被开发出的PVS，是一款集成了多种形式验证的复杂软件，因其优越的性能和强大的功效，因而被成功地使用在如验证飞行控制系统的算法和结构上。（2） 时序逻辑模型检验器：SMV与Spin，SMV是由麦克米兰（McMillan）在1993年发明的，它能够比较有效地表示状态转移系统，被常用于验证工业级别的软硬件系统；而Spin则是由贝尔实验室在1980年开发的面向时序逻辑的检验器，它使用偏向归约方式从而减少系统状态规模，以便来描述验证逻辑的一致性。（3） 行为一致性检验器：FormalChec是作为验证商业模型的检验器。2.定理证明器：（1） 用户指导的自动化推导工具：1994年由考夫曼（Kaufmann）等人开发，既具有数学逻辑又是一个以形式证明和验证的形式化工具ACL2。（2） 证明检验器：由佐敦（Gordon）在上世纪80年代面向硬件验证开发的工具，目前也有面向软件的版本。2.4时间自动机介绍和UPPAAL介绍2.4.1时间自动机时间自动机（Timed Automata，TA）是为了解决实时系统建模和验证而对自动机理论的扩展，由R.Alur和Dill在1994年人提出的理论。TA提供了一种简单有效的描述带有时间因素的系统状态转换图的方法，在实时系统的建模与验证提供了理论依据，在形式化规范说明和模型验证中占据着极其重要的地位2。其中有三种带有时间约束扩展的自动机理论：1）离散事件模型；2）虚拟时钟模型；3）稠密事件模型。2.4.2 UPPAAL的介绍UPPAAL由丹麦的Aalborg大学和瑞典的Uppsala大学在1995年共同开发的，一款具有世界先进水平的实时自动验证工具，其用户界面包括3部分:系统辑器，模拟器和验证器。验证器通过快搜索系统模型的状态空间检查系统的安全可靠性。系统辑器，模拟器和验证器。系统辑器用于创建和吧编辑要分析的系统。模拟器是-个确认工具，检查所建系统模型可能的执行是否有错，以便及时发现错误。形式化方法是能够有效验证系统设计和开发正确性的重要手段之一。目前, 在崇尚形式化方法的欧洲, 大多研究都针对欧洲列车运行控制系统而展开。以德国自然科学基金为基础, 多个大学和研究所联合组成的复杂UPPAAL有一个易于操作和使用的集成环境，其用户界面的四个部分具体定义和功能,编辑器（System Editor）：在编辑器里，创建和编辑需要分析的实时系统，需要创建过程模板，全局声明，过程定义和系统定义。模拟器（Simulator）：对所有可能执行的序列进行检查，对所有系统的状态空间进行检查。验证器（Verifier）：在验证器里，检验系统是否满足规定的功能要求和时间要求，绿色代表通过，红色代表不满足要求。UPPAAL的主要对象包括位置和通道。在时间自动机上改进的是除了原始位置（O）以外，增加了约束位置（Committed location，C）和紧急位置（Urgent location，U）。紧急位置和约束位置与普通位置的区别在于没有时间约束。约束位置可以减少系统状态空间，但是下一个状态必须离开相关的约束位置。紧急位置可以减少模型中的时钟个数以减少分析的难度，但是它常会导致死锁（Deadlock）。位置设置界面如图所示：图2-2 位置设置界面UPPAAL中的通道（Channel）是保证两个或者及其以上多个进程进行互相操作和通信的。通常通道是成对出现的，以“？”结尾的为命令的接受者，而以“！”结尾的为命令的发出者。通道又分为广播通道（broadcast channel)和紧迫通道（urgent channel），紧迫通道向比较普通通道而言没有时间上的延迟，广播通道时存在一对多的通信和交互行为。其中指令（Sync）指的是发出或者接受的命令集合。条件（Guard）指的是通过这条管道的条件，比如必须满足某个值等。更新（Update）指的是完成某个指令后对于某些值或者时间进行重新更新或者清零。通道设置界面如图所示：图2-3 通道设置界面在UPPAAL使用的标准语言是CTL（Computation Tree Logic）语言如下：（1）A P：对于所有的路径，P永远都成立；（2）E P：存在一条路径，使得P永远成立；（3）E P：存在一条路径，使得P最后成立；（4）AP：对应所有路径，P最后成立；（5）PQ：无论何时，P成立则Q成立。无论是建立模型还是模型验证都要依靠这种语言进行建模和验证。CTL是逻辑分支时间，如果没有约束条件，任何一条路径均是可能的路线。第3章 列控系统及其C2/C3等级转换流程分析3.1列控系统的介绍列车运行运行控制系统是铁道智能化的重要组成部分，它根据与先行列车之间的距离和进路条件，在车内连续的显示允许的运行速度，列车按速度的显示自动或者人工控制运行，在该系统中，车载信号直接指示列车应遵守的速度，可靠地防止了因为人为因素事故的发生。列控系统经过地面人工信号、地面自动信号、机车信号、自动停车、速度自动防护、自动驾驶逐渐演变成智能化的系统。在国内外都在快速的发展，其中法国UM2000+TVM430、德国LZB、日本DS-ATC、欧洲ETCS和中国的CTCS是目前世界上主要的列控系统。欧洲的列控系统是ETCS，中国的列控系统是CTCS，CTCS是参照欧盟ETCS标准，中国铁道部组织专家提出的符合我国国情的列控系统。下面主要介绍我国的列控系统CTCS。CTCS是为了保证列车的安全运行，以划分等级的形式满足不同线路的运输需求的列控系统。3.1.1 CTCS的基本功能（1）间隔控制保证追踪列车和前行列车的安全距离。（2）速度防护保证列车的运行速度在允许范围内。（3）安全防护防止列车无行车许可运行、防止列车溜逸、防止列车冒进。行车许可：列车安全运行的行车凭证，包括线路信息和行车距离等。3.2 列控系统基本原理1.列车控制系统的基本组成：车载速度控制设备、车地传输设备、地面列控中心或者无线闭塞中心、轨道电路、地面点式信号设备。地面设备的功能：（1）检测列车的位置。（2）根据进路的情况和前行列车的位置，地面设备计算出列车的允许速度，控制列车运行。（3）向列车传递线路信息和限制速度信息等。车载设备的功能：（1）接收限制速度信息并显示。(2)对列车运行速度进行监督，超过限制速度时，列车自动制动减速，必须保证在限速点前列车的运行速度降到规定值以下。地面列控中心的功能：参考列车的运行位置，前后列车的运行间距产生列控车载系统所需要的地面信息，其中包括列车的目标速度、列车到目标点的距离、线路的坡度和线路的允许速度。车载设备：接收轨道信息或无线传输信息和点式信息，车载设备根据预先输入的列车一些参数，实时计算出列车的当前允许运行速度，并生成速度控制曲线，在司机显示器上显示。列控车载设备能够实时的监测列车当前的运行速度并且在司机显示器上显示，司机依据显示器上的目标速度、目标距离，允许速度和实际速度来控制列车运行。如果列车的实际运行速度超过了当前允许速度，列控车载设备自动控制制动装置，列车制动减速，必须保证列车在停车点前停住，或者在限速点以前把速度降低到限速值以下67。2.列控系统信息传递的方式（1）点式设备点式设备是被广泛传输的一种方式，主要包括点式应答器（有源应答器和无源应答器）和点式环线。工作原理：当机车通过某一位置时，车载应答器天线和地面应答器天线对准，车载应答器发送一定频率的电磁波激活地面应答器，固定位置的地面应答器将储存的列车运行前方的信息调制后通过天线以电磁感应发送给机车。（2）轨道电路轨道电路时列控系统信息传输的传统方式。通过轨道电路和机车上安装的传感器连续的传递信息，并且信息可以随前行列车的状况而及时改变。工作原理：通过轨道电路或则轨间环线连续的传递信息，车载信息接收模块接收到以后并解调后传递给安全计算机，安全计算机根据测速测距模块提供的列车运行速度信息和定位信息生成制动模式曲线，监督列车的运行8。（3）无线传输无线传输是一种采用了先进的通信技术和计算机技术来连续和监测列车运行的移动闭塞方式。工作原理：地面设备通过通信网络向车载设备传递控制信息，车载设备通过通信网络向地面设备传输列车信息，形成闭环的信息传输与控制。数据通信网络可以由多种通信方式组成，比如GSM-R、无线电台、漏泄同轴电缆等等。3.2.1 CTCS的等级划分CTCS体系是以地面设备为基础，包括地面设备和车载设备。CTCS划分为5个等级，CTCS0级-CTCS4级（以下简称C0级-C4级），其中C4级是为满足今后铁路发展预留的。 ( 1 ) CTCS0级 由通用运行监控记录装置和机车信号构成。 既有线现状 。 适用于速度不超过160km/h。 ( 2 ) CTCS1级 由安全型运行监控记录装置和主体机车信号组成。 机车乘务员凭车载信号行车。 适用于速度不超过160km/h。 ( 3 ) CTCS2级 基于轨道电路和应答器传输列控信息。 用于速度为200-250km/h线路。 动车组之间的追踪间隔缩短至5分钟。 已成功应用于第六次提速，时速 200公里及以上线路里程6227公里，其中时速250公里线路里程1019公里9。 ( 4 ) CTCS3级 基于无线通信平台传输列控信息。 轨道电路实现列车占用检查。 机车乘务员凭车载信号行车。 用于300-350km/h线路。 动车组间的追踪间隔缩短至3分钟。( 5 ) CTCS4级 基于无线通信平台传输列控信息。 实现虚拟闭塞或移动闭塞。 取消轨道电路。 是中国铁路未来发展方向。3.2.2 CTCS-2级列控系统工作原理1.CTCS-2级列控系统的组成：（1）地面子系统a.列控中心根据进路情况和列车占用状况，计算出列车行车许可和列车运行静态曲线，并发送给列车。b.轨道电路完成列车完整性检查和占用检查，连续的向列车传送控制信息。车站和区间采用同制式轨道电路。c.点式信息设备向车载设备传输线路参数、选录参数、定位信息、限速和停车等消息。2.车载子系统a.连续信息接收模块用于轨道电路信息的传输和处理。b.点式信息接收模块用于点式信息的接收和处理。常用定位技术：轨道电路定位、查询应答器定位、测速定位等c.测速模块监测列车的车速和走行距离。d.设备维护记录单元记录信息、系统状态和控制动作。e.车载安全计算机综合处理列车控制信息，生成目标距离牧师曲线，控制列车运行10。f.人机界面车载设备与司机交互设备。h.运行管理记录单元记录运行相关数据，规范司机驾驶。g.预留无线通信接口2.系统工作原理车载列控中心将线路参数、限速命令和进路状况等信息通过有源应答器传递给列车，轨道电路完成列车占用检测和完整性检测，并将行车许可传递给车载设备，车载设备综合地面设备提供的线路参数、进路参数和限速信息等生成目标距离模式曲线和控制速度，控制列车运行。3.2.3 CTCS-3级列控系统工作原理1.CTCS-3级相比较CTCS-2级列控系统，增加的设备组成：（1） 地面子系统无线闭塞中心（RBC)和GSM-R无线通信网络基于无线通信方式的地面列车间隔控制系统，根据进路状况和列车占用情况向锁管辖列车发送行车许可和控制信息。（2） 车载子系统GSM-R无线通信单元实现车-地双向大容量的信息传输。2.系统工作原理车载联锁根据轨道电路的占用信息和线路参数给出信号授权，传递给无线闭塞中心，行调指挥中心（CTC）综合列车相关信息给出限速信息也传递给无线闭塞中心，无线闭塞中心将其传递给车载设备，车载设备实时计算出列车的运行控制曲线，控制列车运行。第4章 C2/C3等级转换过程建模与验证4.1列控系统的等级转换过程列控系统的等级转换，总体来看包括两个方面：1.固定位置的等级转换列车在行车过程中，由于线路情况的不同，列车需要从C0/1线路进入C2线路，从C2进入C0/1线路，或则从C2进入C3线路，从C3进入C2线路。车载设备经过一个固定位置时，从该位置的固定应答器接收等级转换的信息，并进行等级转换。2.设备故障后降级运行列车在运行过程中，经过某个位置时关键设备发生故障，为了保障列车安全运行，列车必须自动降级，根据“故障-安全”原则，从C3切换到C2，从C2切换到C0/1。4.1.1固定位置等级转换1.列车在运行的过程中，由于线路情况的转变，列车需要从C2线路进入到C3线路时，或者列车需要进行C2到C3等级转换。图4-1 C2/C3等级转换应答器组和确认区设置示意图当列车接近在固定入口位置设置的RBC连接应答器（RL）时，RL应答器向列车发送命令，命令列车和无线闭塞中心(RBC）相连接，如果呼叫成功则进行连接，并转入C3级行车，否则列车依然以原模式运行。当列车经过预告应答器（YG）时，RBC向车载设备传递行车参数、线路许可和等级转换命令，车载设备向RBC传递列车的位置等信息。C3控制单元接受到等级转换位置信息后，在距离转换执行点的一定距离的位置，提示司机进行C2-C3等级转换确认，司机进行转换确认。当列车到达等级转换执行应答器组（ZX）时，自动转换为C3行车，司机随即进行确认，但是确认时间在5秒内，随后列车将根据C3控制单元计算的线路数据和行车许可行车。2.从C3到C2的转换。列车驶出C2线路区域进入C3线路区域时，当其经过预先设定在固定位置的等级转换预告应答器时，接收到无线闭塞中心发出的C3到C2等级切换的命令。列车进入等级转换准备阶段。当列车经过等级转换应答器时，自动进入C2行车。当列车的尾部离开等级转换应答器时，车载设备断开与RBC的连接。3.从C2到C0/1的转换。当列车由C2线路区域进入到C0/1线路区域时，先要经过在一定距