毕业设计（论文）-基于UPPAAL的区域控制器功能建模与验证.doc

西西 南南 交交 通通 大大 学学 本本 科科 毕毕 业业 设设 计计 (论论 文文) 基于 UPPAAL 的区域控制器功能建模与验证 MODELING AND VERIFICTION OF ZONE CONTROLLER FUNCTION BASED ON UPPAAL 年 级: 2010 级 姓 名: 专 业: 通信工程（铁道信号） 指 导 老 师: 二零一四年六月 承承 诺诺 本人郑重承诺：所呈交的设计（论文）是本人在导师的指导下独立 进行设计（研究）所取得的成果，除文中特别加以标注引用的内容外， 本文不包含任何其他个人或集体已经发表或撰写的设计（研究）成果。 对本设计（研究）做出贡献的个人和集体，均已在文中以明确方式标明。 如被发现设计（论文）中存在抄袭、造假等学术不端行为，本人愿承担 一切后果。 学生签名： 年 月 日 院 系 计算机与通信工程系 专 业 通信工程（铁道信号） 年 级 2010 级 姓 名 温成 题 目 基于 UPPAAL 的区域控制器建模与验证 指导教师 评 语 指导教师 (签章) 评 阅 人 评 语 评 阅 人 (签章) 成 绩 答辩委员会主任 (签章) 年 月 日 西南交通大学本科毕业设计(论文) 第 I 页 毕业设计（论文）任务书毕业设计（论文）任务书 班 级 2010 级 学生姓名 温成 学 号 20108103 发题日期： 2014 年 2 月 21 日 完成日期：2014 年 6 月 5 日 题 目 基于 UPPAAL 的区域控制器功能建模与验证 1、本论文的目的与意义 对于整个铁道系统，安全与高速是整个系统核心目标。特别是在 2011 年“7.23 甬温线特别重大铁路交通事故”后，铁道信号控制领域越来越受到铁路安全部门和 乘客的关注。本论文以基于无线通信的列车控制系统中区域控制器间切换为切入点 建模、验证、分析了切换时区域控制器与其他子系统通信的过程。为其软件设计时 提供了参考和指导，可以消除部分系统设计之初时的逻辑矛盾、定义模糊、功能混 乱等情况，这样可以提高区域控制器工作的安全性和可靠性。 2、学生应完成的任务 了解区域控制器的作用与标准； 了解形式化验证在国外的研究现状； 明确形式化验证的多种方法； 利用软件对区域控制器间切换建模与验证； 对已得到的结果进行分析。 西南交通大学本科毕业设计(论文) 第 II 页 3、论文各部分内容及时间分配：（共 18 周） 第一部分查阅 UPPAAL、形式化验证、区域控制的相关文献 ( 1 周) 第二部分对查阅资料进行分类、构建设计思路、撰写论文提纲 ( 2 周) 第三部分利用 UPPAAL 对区域控制器系统进行建模 ( 4 周) 第四部分读模型进行验证和修改、开始撰写毕业论文 ( 6 周) 第五部分论文完善及排版修改 ( 2 周) 论文评阅及答辩 ( 2 周) 论文整改 ( 1 周) 备 注 指导教师： 年 月 日 审 批 人： 年 月 日 西南交通大学本科毕业设计(论文) 第 III 页 摘 要 铁道信号系统是铁路系统中极其重要的一环。它的主要工作是指挥列车运行、 保证行车安全、提高运输效率等。其中，基于无线通信的列车控制系统的发展是铁 道信号系统未来的主要发展趋势。作为 CBTC 的核心设备，区域控制器是生成移动 授权与发送。区域控制器的工作是否满足行车需求，决定了整个铁道信号系统的安 全性与可靠性。本论文是在解析了 CBTC 的工作原理，分析了区域控制器与其他子 系统的通信关系，以区域控制器为研究对象，进行建模、仿真、分析与验证。 本论文首先介绍了 CBTC 系统和区域控制器的工作原理，并提出了为什么需要 对系统进行可靠性验证；概括性地介绍了形式化方法在国外的发展势态；介绍了本 论文的研究目的与大体结构。 本论文介绍了形式化验证的概念、分类与发展历史，根据验证方法的不同流派 介绍了形式化验证的一些常见工具，并且着重介绍了时间自动机方法及代表软件 UPPAAL。 基于此工具本论文将详细分析了区域控制器的工作原理、与其他子系统的通信 过程。基于此，利用 UPPAAL 软件对整个系统流程进行了建模、仿真、验证与分析， 并且得出了验证与分析结果。 最后根据验证与分析结果，从而可以为设计人员在初期设计时避免设计的不一 致性、模糊性与不完备性。为设计人员提供了参考与指导。 关键词 区域控制器；移动授权；形式化方法；UPPAAL 西南交通大学本科毕业设计(论文) 第 IV 页 Abstract Railway signal systems in the railway system is an extremely important part. Its main work is to command the train operation , ensure traffic safety, improve transport efficiency and so on. Among them, the development of the train control system based on communication is the next major development trend of railway signal systems. As the core equipment of CBTC, zone controller is generated and sent movement authority. Whether Zone controller can meet the needs of work , determine the safety and reliability of the railway signal systems. This paper is in the works to resolve the CBTC, analyzes the relationship between zone controller and other sub systems, zone controller is to be the object, to model, simulate, analysis and verify. This paper introduces the principle of CBTC and zone controller system and proposes why do we need to verify the reliability of the system; general introduces the description of the development of formal methods in foreign country; introduces the purpose and general structure of the paper. This paper introduces the concept, classification and history of formal verification, according to different methods, introduces some tools of the formal verification, and focuses on the timed automat and on behalf of the software UPPAAL. This paper analysis the working principle of the zone controller, and the communication process with other subsystems. Based on this, use UPPAAL to process the entire system to model, simulate, verificy and analysis, and we can have the results of the verification and analysis. Finally, based on the results of verification and analysis, allowing designers to avoid inconsistencies, ambiguity and incompleteness in the early design. Guide Offers designers a reference . Key words Zone Controller; movement authority; formal Methods; UPPAAL 西南交通大学本科毕业设计(论文) 第 V 页 目目 录录 第 1 章 绪论.1 1.1 CBTC 系统.1 1.1.1 CBTC 系统介绍.1 1.1.2 系统可靠性验证的必要性.2 1.1.3 区域控制器系统介绍.3 1.2 国内外形式化方法发展概况 .4 1.3 研究目的与论文内容 .5 1.3.1 研究目的.5 1.3.2 论文安排.5 第 2 章 形式化方法与运用.7 2.1 基本概念 .7 2.2 形式化工具 .8 2.3 时间自动机（TA）介绍和 UPPAAL 介绍 .8 2.3.1 时间自动机.8 2.3.2 UPPAAL 介绍 .9 第 3 章 基于 UPPAAL 的区域控制器切换流程建模验证 .12 3.1 区域控制器间切换流程 .12 3.1.1 区域控制器工作状态.12 3.1.2 MA 计算.13 3.1.3 ZC 与其他子系统的信息交互.13 3.1.4 ZC 间切换的详细过程.14 3.1.5 准备移交的区域控制器 ZC1.15 3.1.6 准备接管的区域控制器 ZC2.17 3.1.7 车载控制器 VOBC.20 3.1.8 计算机联锁 CI.23 3.1.9 列车自动监控系统 ATS .25 3.1.10 轨旁设备 RE.28 西南交通大学本科毕业设计(论文) 第 VI 页 3.1.11 数据存储单元系统 DSU.29 3.1.12 全局变量的设定.30 3.2 区域控制器间切换流程模拟仿真 .31 3.2.1 ZC1 发送预切换通信和 ZC2 回复.32 3.2.2 ZC1 请求计算 MA .33 3.2.3 ZC2 与 VOBC 建立通信和 ZC1 注销.33 3.2.4 VOBC 正式向 ZC2 办理接管手续.34 3.2.5 故障处理.34 3.3 区域控制器切换流程形式化验证与分析 .35 3.3.1 逻辑功能性验证.36 3.3.2 时序功能性验证.37 3.3.3 安全性验证.38 结论和展望.39 结论.39 展望.40 致 谢.41 参考文献.42 附 录.43 图引索.43 表引索.43 西南交通大学本科毕业设计(论文) 第 1 页 第 1 章 绪论 1.1 CBTC 系统 1.1.1 CBTC 系统介绍 进入 21 世纪后，中国中央政府根据现代社会发展需求，在 2004 年经国务院批 准了中长期铁路网规划 ，目标是在 2020 年全国铁路营业里程数达到十万公里1。 通过近几年的高速铁路的快速发展，中国已成为了全世界高速铁路发展最快、运营 里程最长、运营速度最高、技术发展最迅猛的国家。作为与人民生活息息相关的轨 道交通产业，安全与高速这两个目标是整个系统核心追求。轨道交通系统的安全性 取决于列车运行控制系统中列车定位的精确性和安全性。其中基于通信的列车运行 控制系统（Communication Based Train Control, CBTC）经过多年的快速发展，取得 了长足的发展2。包括英国伦敦、法国巴黎、美国纽约、日本东京、加拿大温哥华、 中国北京、香港等多个城市均使用了来自阿尔卡特、西门子、阿尔斯通、卡斯柯等 厂商研发的列车控制系统。多年前由美国电气电子工程师协会轨道交通运输车辆接 口委员会（IEEE Rail Train sit Vehicle Interface Standards Committee, IEEE RTVISC） 制定了 CBTC 通用标准，如图 1-1 所示3。 整个系统包括了车载设备和地面设备两个部分，车载设备与地面设备通过“数 据通信网络”连接，构成了系统的核心。典型框图中还列出了“联锁” 、 “相邻的 CBTC 地面设备” 、 “ATS 系统”等设备，完善了 CBTC 系统的功能。实际系统根据 厂家和实际情况的不同可能有略有差异，但是列控系统的核心功能框图都是一致的。 西南交通大学本科毕业设计(论文) 第 2 页 ATS系统 相邻CBTC 地面设备 CBTC 地面设备 联锁 数据通信网络 列车运行控制 CBTC 车载设备 列车子系统 与相邻联锁相连 图 1-1 经典 CBTC 框架图 1.1.2 系统可靠性验证的必要性 随着我国高速铁路网络“四纵四横”基本框架的建成，中国中央政府又提出了 “八纵八横”的新的规划要求4，可以见得未来几年仍然是我国高速铁路的加速建 设时期，既有高速铁路、修建中的高速铁路和规划中的高速铁路总里程将远远超过 德国、法国、日本等传统高速铁路强国。 高速铁路技术的引进、模仿和自主创新都涉及了大量的技术难题，高速铁路的 最快速度高达 350km/h。特别是在 2011 年“7.23 甬温线特别重大铁路交通事故”后 5，铁道通信和信号系统的安全性与可靠性越来越受到重视，因为任何细小的故障 都会给国家和人民生命财产造成难以弥补的损失。所以，为了让中国高速列车继续 以高安全性运行，就必须对列车运行控制系统技术的各个系统深入研究，提高系统 的安全性与可靠性，确保万无一失。 而对安全苛求系统，如轨道交通控制系统、航空航天控制等应用，传统的软件 开发方法难以开发出高安全性的软件。随着对计算机系统安全技术研究的深入，国 外有关学者己把和安全功能相关的计算机系统看作安全苛求系统（Safety Critical System）进行单独研究，提出了很多提高系统安全性能的技术方法。安全苛求系统 是指对组成系统的软件、硬件安全性级别要求很高的计算机、电子或电气系统，系 西南交通大学本科毕业设计(论文) 第 3 页 统出现故障后可能导致人员伤亡、重大经济损失或环境破坏等严重后果。轨道交通 信号系统是一种典型的安全苛求系统。 鉴于上述情况，人们提出在软件的需求规范、设计和验证中均引入具有清晰的 数学基础的严格的技术和工具，也即形式化方法（Formal Methods） 。这里的“具有数 学基础的严格性”是指软件规范采用基于数学逻辑的形式化的描述形式，而且软件的 验证也是采用该数学逻辑严格推导出来的（即软件执行的每一步都遵循特定的推导 规则，因此可以由计算机自动来进行验证） 。 形式化方法的重要意义在于提供了一种可以确信地检验软件的全部状态空间， 而且说明软件的某项正确性或者安全性特征对所有可能的输入都成立的方法。 列控系统是铁道信号的核心系统，本论文将结合区域控制器，特别是区域控制 器切换的形式化可靠性验证为切入点做出形式化描述、建模、验证和分析。 1.1.3 区域控制器系统介绍 区域控制器（Zone Controller，ZC）是 CBTC 系统的地面设备的核心部分，可 实现车站与相邻车站的联锁和 ATP 控制。它对系统的安全性和可靠性有着极高的要 求。ZC 工作是否稳定直接影响着列车运行效率与安全。ZC 的主要功能是对固定区 域的列车进行管理，包括：列车登入、列车受控、提供移动授权（Movement Authority，MA）等。与 ZC 相互通信的其他子系统还包括：6 （1）列车自动监控系统子系统 列车自动监控子系统（Automatic Train Supervision，ATS）的主要功能是对于列 车运行以及道岔、信号机等设备的状态监控，并且显示控制范围内列车运行状态信 息和运行时刻表。 （2）计算机联锁子系统 计算机联锁子系统（Computer Interlocking，CI）的主要功能是进路控制、道岔 控制、信号控制、轨道空闲处理等。 （3）车载控制器子系统 车载控制器子系统（Vehicle On Board Controller,VOBC）是主要功能是控制列 车运行，并且记录列车的位置和运行方向等信息，列车定位是采用测速传感器和地 面应答器相结合的方式实现的。 西南交通大学本科毕业设计(论文) 第 4 页 （4）数据存储单元子系统 数据存储单元系统（Data Saving Unit，DSU）是地面与列车共用的一个数据库。 这个数据库存储了列车与地面的各种信息，ZC 会调用数据库内的静态与动态数据。 ZC 与其他子系统的交互信息流图如图 1-2 所示： ZC系统相邻ZCATS VOBC CI MA申请 MA信息 跨区运行 列车信息 确认信息 ZC信息 临时限速 列车设别号 列车信息进路信息 图 1-2 交互信息流图 1.2 国内外形式化方法发展概况 自从计算机面世以来，在各个领域，特别是工业方面得到了迅速的发展，它在 人类物质文化生产中极速地提高了生产效率，使得产品的研发周期越来越短和功能 越来越复杂，但与此同时也带来了安全隐患。在铁路工业发展方面，铁道信号系统 的复杂度也越来越高，一旦发生故障造成的损失也越来越大。此时，急需一种研究 方法对整个系统的安全性、可靠性进行完善地分析与验证 Error! Reference source not found.。 目前，世界上许多高校与研究院的学者普遍倾向于使用基于数学的形式化方法来解 决这个难题。 经过生产实践与产品的优胜劣汰，特别是在本世纪以后仍然在研究界有一定活 力的方法与工具，将成为往后形式化方法发展的主要流派。 形式化发展最早起源于上世纪 50 年代后期，巴克斯提出了巴克斯范式（BNF） 西南交通大学本科毕业设计(论文) 第 5 页 作为描述程序语言语法的元语言。在 60 年代，佛洛依德等人开展的程序正确性证明 研究推动了形式化方法的发展，他们利用数学方法来证明程序的正确性并以此为基 础研究发展了多种程序验证方法。到了 80 年代，在硬件设计领域形式化方法的工业 应用结果掀起了软件形式化开发的学术研究的热潮，其中有代表的一个项目就是 IBM 商用信息控制系统，给整个开发工作节约了 9%的成本并且大幅提高了产品质 量并且减少了错误率。往后在各个领域（比如计算机、军事、汽车、民航等）形式 化研究方法都得到了长足的发展，研究方法也呈多样化趋势8。 在国内，形式化方法的研究起步较晚，但发展迅速，并在某些安全苛求的系统 应用中取得了有益的成果。华东师范大学何继丰院士团队等对模型驱动的软件开发 技术、形式化验证、模型检查等进行了深入研究，并开始为国内的华为、上海贝尔 等企业的形式化方法应用提供技术支持。北京交通大学应用时间自动机模型对列车 运行控制系统进行建模，通过对模型检验和定理证明方法的比较，认为模型检验方 法比较适合作为列车运行控制系统形式化验证的方法。 1.3 研究目的与论文内容 1.3.1 研究目的 本论文的主要是研究目的是：研究在 CBTC 系统中作为核心的区域控制器 ZC 在 CBTC 的系统框架下，根据 ZC 子系统的功能需求、安全性需求、可靠性需求， 完成 ZC 子系统的可靠性软件验证。先对 ZC 子系统与其他子系统规范描述，通过相 关形式化软件建模，并且对建立好的模型进行形式化验证。通过验证分析并且找到 实际运行中可能存在的安全漏洞，作为相关设计的参考，以便不断提高设计的安全 性与可靠性，最终达到相关安全系统的验收标准。 1.3.2 论文安排 本论文安排如下： （1）第一章 绪论，简要介绍 CBTC 系统的主要结构、ZC 子系统、与 ZC 子系 统相互通信的其他子系统、国内外可靠性验证的发展现状与历史，给出论文的研究 目的及内容。 西南交通大学本科毕业设计(论文) 第 6 页 （2）第二章 形式化方法与运用，简要介绍世界主流的可靠性验证形式化方法 及对应的软件和工具。本论文主要是运用 UPPAAL 软件，所以会着重介绍 UPPAAL 软件以及它的核心思想。 （3）第三章 建模与验证，本论文将选取 ZC 之间的转换为切入点，说明 ZC 转 换时的数据通信原理及过程，与其他子系统的通信关系与逻辑。利用形式化软件建 立相对应的模型，并且设置大量的各种类型的故障，最后进行形式化可靠性验证， 得出分析结果，为完善系统设计提供参考与依据。 （4）结论和展望 （5）参考文献及附录 西南交通大学本科毕业设计(论文) 第 7 页 第 2 章 形式化方法与运用 2.1 基本概念 形式化方法是用于规范、设计与验证并且基于数学的计算机验证方法，包括了 多种语言、技术与工具。如图 2-1，是经典的形式化方法示意图9。 形式规范形式验证器 系统特征 系统验证 正确/错误？ 图 2-1 经典形式化方法示意图 形式化方法主要包括两大流派：形式化规范方法与形式化验证方法两大类。 （1）形式化规范（Formal Specifition）方法，包括各种基于数学的表示法，以 及对应的规范语言与工具。 规范是一个描述系统和特性的过程，规范的语言是用来描述系统。规范语言有 具有严格定义的语法与语义。系统特性包括：行为特性、性能特性、时间特性、内 部结构等。它大概可以分为三大类： 1）描述顺序系统行为的形式规范方法； 2）描述并发系统行为的形式规范方法； 3）集成的形式规范方法。 （2）形式化验证（Formal Verifition）方法，包括各种模型验证器，以及对应的 证明器、方法和工具。 形式验证是指的严格数学方法来推理验证产品或设计是否符合其全部或部分规 范的过程。形式验证要求产品的规范和实现需要有严格的形式描述。主要有两种方 法： 1）模型验证（Model checking） ，采用一种规范的形式语言，构造一种算法 建立根据设计的模型，确认模型是否满足规范说明。 2）定理验证（Theorem proving） ，先是定义一种数学逻辑，该逻辑其实是 西南交通大学本科毕业设计(论文) 第 8 页 一种形式化的系统，由若干的公理和推理规则组成。利用数学逻辑来表示被验 证的系统和被期望的特性。其过程就是用现有的规则和公理逐步推出我们需要 的特性。 形式化方法有四个主要的方法源头：1）公理（Axion）方法；2）模型方法 （Model）方法；3）计算（Calculus）方法；4）代数（Algebra）方法。 2.2 形式化工具 前文提到了形式化验证分为两个大类：模型检验与定理证明，本论文主要介绍 其具有代表性的工具：9 （1）模型检验工具： 1）时序逻辑模型检验器：SMV 与 Spin，1993 年由麦克米兰（McMillan） 发明的 SMV，能够比较有效地表示状态转移系统，常用于验证工业规模的软硬 件系统；而 Spin 则是由贝尔实验室实验组在 1980 年开发面向时序逻辑检验器， 使用偏向归约方式减少系统状态规模，以便描述验证逻辑的一致性。 2）行为一致性检验器：其代表是 Formal Check，一个主要验证商业模型的 检验器。 3）组合验证器：上世纪 80 年代开发的 PVS，是一款集成了多种形式验证 的复杂软件，由于其优越的性能，成功地使用在如验证飞行控制系统的算法和 结构上。 （2）定理证明器： 1）用户指导的自动化推导工具：1994 年由考夫曼（Kaufmann）等人开发， 具有数学逻辑又是一个以形式证明和验证的形式化工具 ACL2。 2）证明检验器：由佐敦（Gordon）在上世纪 80 年代开发面向硬件验证的 工具，目前也有面向软件的版本。 2.3 时间自动机（TA）介绍和 UPPAAL 介绍 2.3.1 时间自动机 时间自动机（Timed Automata，TA）由 R.Alur 和 Dill 在 1994 年人提出的理论， 西南交通大学本科毕业设计(论文) 第 9 页 是为了适应实时系统的验证需求，从而解决实时系统建模和验证而对自动机理论的 扩展10。TA 提供了一种简单有效的方法描述带有时间因素的系统状态转换图，在 实时系统的建模与验证提供了理论依据，在形式化规范说明和模型验证中有着极其 重要的地位。其中有三种带有时间约束扩展的自动机理论：1）离散事件模型；2） 虚拟时钟模型；3）稠密事件模型。 2.3.2 UPPAAL 介绍 UPPAAL 由丹麦的奥尔堡（Aalborg）大学和瑞典的乌普萨拉（Uppsala）大学 在 1995 年共同开发的，一款具有世界先进水平的实时自动验证工具1112。它用于 可以被描述为非确定的并行过程的积的系统。每个过程被描述成由有限控制结构、 实数据时钟和变量组成的时间自动机，通过管道和变量互相通信。UPPAAL 的模拟 检测引擎，基于 C 和 C+技术实现的，图形界面在 JAVA 环境下执行，两部分通过 TCP/IP 通讯。UPPAAL 有一个易于操作和使用的集成环境，用户界面主要包括四个 部分： （1）编辑器（System Editor）：在编辑器里，时间自动机模型被称为并发的系 列进程，进程通过参数模板实例化。我们通过对通道和变量的设置完成模型的建立。 （2）模拟器（Simulator）：在模拟器里，用户可以模拟运行并且再过过程中选 择迁徙，通过查看运行轨迹来检验是否可达到。 （3）模拟器 2（Concrete simulator）：和模拟器 1 的功能差不多，是 2013 年最 新版本才具有的，具体功能本论文作者尚未开发，所以暂时不用。 （4）验证器（Verifier）：在验证器里，用户可以对系统属性在模型中检验， 灰色代表尚未验证，绿色代表通过，红色代表不满足要求。 在 UPPAAL 中对时间自动机的位置有了一定的改进，除了原始位置（O）以外， 还增加了约束位置（Committed location, C）和紧急位置（Urgent location, U） 。紧急 位置和约束位置与普通位置的区别在于没有时间的流逝。使用约束位置可以减少系 统状态空间，但是下一个状态必须离开相关的约束位置。而使用紧急位置可以减少 模型中的时钟个数以减少分析复杂度，它常会导致死锁（Deadlock） 。位置设置界面 如图 2-2 所示： 西南交通大学本科毕业设计(论文) 第 10 页 图 2-2 位置设置界面 其中名称（Name）在一个编辑器内是唯一的，系统不能识别两个相同的名称。 在实际运用当中可以用后缀“_”（比如 RM_区分于 RM）加以区分。不变量 （Invariant）是指的通过这个位置的时间限制。 在 UPPAAL 中的通道（Channel）是极其重要的，通过通道保证两个或者更多 的进程的同步通信和交互。通常一个通道是成对出现的，以“！”结尾的为命令的 发出者，而以“？”结尾的为命令的接受者。管道设置界面如图所示： 图 2-3 管道设置界面 其中条件（Guard）指的是通过这条管道的条件，比如必须满足某个值等。指令 （Sync）指的是发出或者接受的命令集合。更新（Update）指的是完成某个指令后 对于某些值或者时间进行重新更新或者清零。 在 UPPAAL 使用的是比较简单的 CTL（Computation Tree Logic）语言，无论是 模型的建立还是验证都必须使用这种语言。CTL 是逻辑分支时间，在没有约束下， 任何一条路径均是可能的路线。在后期验证的过程中一般会用到以下的语句： （1）A P：对于所有的路径，P 永远都成立； 西南交通大学本科毕业设计(论文) 第 11 页 （2）E P：存在一条路径，使得 P 永远成立； （3）E P：存在一条路径，使得 P 最后成立； （4）A P：对应所有路径，P 最后成立； （5）PQ：无论何时，P 成立则 Q 成立。 西南交通大学本科毕业设计(论文) 第 12 页 第 3 章 基于 UPPAAL 的区域控制器切换流程建模验证 3.1 区域控制器间切换流程 3.1.1 区域控制器工作状态 本论文第一章已经提到了 ZC 的基本原理做了介绍，ZC 需要对在其管辖范围内 的列车进行控制和管理，针对不同的实际情况，ZC 有四种工作状态，我们可以分为 以下四种情况13： （1）列车预登录：列车在准备出车辆段时候，列车以 RM（Restricted Train Operating Mode，限制人工驾驶模式）运行。当列车与 CBTC 区域预告应答器互相 通信时，代表列车已经进入本区域 ZC 的管辖范围，VOBC 会查询 DSU 数据库的信 息，申请登入本区域的 ZC，ZC 接收到申请后，会与 ZC 自身的数据库中的列车 ID 等相匹配查询，如未有相匹配信息，代表该列车是第一次登陆 ZC，此时列车状态即 为列车预登陆。 （2）列车进入 ZC 控制：当 VOBC 发出申请并且收到确认回复后，列车保持 RM 模式运行，列车与 CBTC 区域执行应答器互相通信后，VOBC 将向 ZC 发送列 车动态信息（比如列车速度、位置和方向） ，并且发出区域控制器的受控请求。期间， ZC 与 VOBC 仅发空白报文来保持联系。 （3）ZC 正式控制列车：ZC 与 CI 互相通信，报告列车位置信息，请求进路， 进路排通后，ZC 将计算 MA，VOBC 收到 MA 后，此时列车正式成为本区域 ZC 管 理的列车了。 （4）列车注销：列车离开 ZC 的管辖范围内或者列车将进入车辆段时，列车处 于注销状态。在此过程中，ZC 会清除列车