(19)国家知识产权局 (12)发明 专利申请 (10)申请公布号 (43)申请公布日 (21)申请 号 202211432332.8 (22)申请日 2022.11.16 (71)申请人 华侨大学 地址 362021 福建省泉州市城华北路269号 (72)发明人 陈祖希　牛传军　梅萌　骆翔宇　 郑黎晓　周长利　徐中伟　 (74)专利代理 机构 北京高沃 律师事务所 1 1569 专利代理师 万慧华 (51)Int.Cl. G05B 23/02(2006.01) G06F 30/20(2020.01) G06F 30/15(2020.01) (54)发明名称 一种自主列车运行控制系统建模及验证方 法 (57)摘要 本发明公开了一种自主列车运行控制系统 建模及验证方法， 属于轨道交通系统建模领域。 该方法包括： 对自主列车运行控制系统进行分 析， 得到自主列车运行控制系统分析图； 基于所 述自主列车运行控制系统分析图对所述自主列 车运行控制系统进行非形式化描述； 基于所述非 形式化描述对所述自主列车运行控制系统进行 建模； 采用Event ‑B形式化方法对所述自主列车 运行控制系统的模型进行优化； 通过Rodin平台 中的定理证明器对优化后的自主列车运行控制 系统的模型进行证明。 本发明基于抽象数据类型 （ADT） 与Event ‑B方法的精化策略对自主列车运 行控制系统进行建模， 利用AD T的抽象概念， 能够 有效弥补单一使用精化策略的不足之处。 权利要求书1页 说明书8页 附图3页 CN 115494829 A 2022.12.20 CN 115494829 A 1.一种自主列车运行控制系统建模及验证方法， 其特 征在于， 包括： 对自主列车运行控制系统进行分析， 得到自主列车运行控制系统分析图； 基于所述自主列车运行控制系统分析图对所述自主列车运行控制系统进行非形式化 描述； 基于所述非形式化描述对所述自主列车运行控制系统进行建模； 采用Event ‑B形式化方法对所述自主列车运行控制系统的模型进行优化； 通过Rodi n平台中的定理证明器对 优化后的自主列车运行控制系统的模型进行证明。 2.根据权利要求1所述的自主列车运行控制系统建模及验证方法， 其特征在于， 所述自 主列车运行控制系统包括列车、 区段资源和资源管理器； 在所述自主列车运行控制系统中， 所述列车的移动包括： 资源请求、 资源分配以及资源释放； 在所述资源请求阶段， 所述列车向所述资源管理器请求 运营任务中的所述区段资源； 在所述资源分配阶段， 所述资源管理器将所述区段资源分配至对应的所述列车； 在所述资源释放阶段， 所述资源管理器将所述列车从排序队列中移除， 若释放的区段 资源为线性区段时， 则将列车的移动授权范围缩小， 若释放的区段资源为道岔区段时， 则将 列车的移动授权范围缩小且所述资源管理器将所述道岔区段 的定位侧防区和反位侧防区 的方向锁闭进行释放。 3.根据权利要求1所述的自主列车运行控制系统建模及验证方法， 其特征在于， 所述自 主列车运行控制系统的模型包括9层， 每层 模型具有不同的需求规约， 且每层模 型待验证的 性质也不同。 4.根据权利要求3所述的自主列车运行控制系统建模及验证方法， 其特征在于， 所述自 主列车运行控制系统的9层模型分别为模型M0_active_net、 模型M1_train、 模型M2_ma、 模 型M3_req、 模型M4_queue、 模型M5_point、 模型M6_direction、 模型M 7_collision_free以及 模型M8_derai lment_fre e。 5.根据权利要求4所述的自主列车运行控制系统建模及验证方法， 其特征在于， 所述采 用Event‑B形式化方法对所述自主列车运行控制系统的模型进行优化， 具体包括： 建立轨道网络以及区域Regi on ADT； 所述模型M 0_active_net关注于所述自主列车运行控制系统中活动的所述轨道网络； 所述模型M1_train、 所述模型M2_ma以及所述模型M3_req分别将列车、 MA以及列车请求 区段资源的集 合使用所述区域Regi on ADT表示； 所述模型M4_queue、 模型M5_point和M6_direction中逐层引入所述自主列车运行控制 系统的排序队列、 资源细分和方向锁闭的性质； 所述模型M7_collision_free和模型M8_derailment_free考虑所述自主列车运行控制 系统的无碰撞、 无侧冲以及无脱轨的安全属性。权　利　要　求　书 1/1 页 2 CN 115494829 A 2一种自主列车运行控制系统建模 及验证方 法 技术领域 [0001]本发明涉及轨道交通系统建模技术领域， 特别是涉及一种自主列车运行控制系统 建模及验证方法。 背景技术 [0002]列车自主运行控制系统 （Train  Autonomous  Circumambulate  System， TACS） 以车 车通信为基础， 以车载控制为核心， 实现列车自主进路、 自主防护、 自主调整等核心功能， 打 破了传统的基于通信的列车控制系统 （Communcation  Based Train Control System， CBTC） 固有限制。 通过软件计算、 网络通信和自动化控制三大技术的协同， 提供更加 灵活且 细粒度的列车控制、 连续的安全列车间隔保证和超速防护， 促使列车可以在更短的运行间 隔内进行追踪运行， 极大地提升了轨道交通运输的效率和 安全保障。 与其他制式的列车控 制技术相比， 由于追求细粒度的车辆控制和更密集的车辆运能投放， TACS系统的精准性需 求更高、 实时性更强、 安全性需求变得尤为突出。 此外， 由车 ‑车及车‑地之间无线通信方式 而引入的众多不确定因素， 更加深 了解决这些问题的难度。 作为TACS系统的核心组成部 分， TACS系统软件的正确性、 安全性和可靠性 直接关系到整个系统的成败。 [0003]对于轨道交通系统建模， 由于其物理环境与系统行为的复杂性， 在形式化建模与 验证过程中极易发生状态空间爆炸 问题。 这使得保证轨道系统安全性变得十分困难。 目前 对于轨道交通系统的建模与验证的研究中， Ev ent‑B是主流的、 获得工业界认可的形式化方 法， 将Event ‑B方法用于CTBC系统的研究较多， 由于TACS系统的新颖性， 还未有研究人员将 Event‑B方法用于TACS系统的形式化建模与验证。 但从CBTC系统的形式化建模与验证研 究 来看， 单一使用Event ‑B方法的精化策略仍然存在建模过程冗长、 证明复杂度过高的问题。 相较CBTC系统， TACS系统更为复杂， 如果单一使用Event ‑B方法对TACS系统进行证明， 上述 问题会被进一 步扩大。 发明内容 [0004]基于此， 本发明的目的是提供一种自主列车运行控制系统建模及验证方法。 [0005]为实现上述目的， 本发明提供了如下 方案： 一种自主列车运行控制系统建模及验证方法， 包括： 对自主列车运行控制系统进行分析， 得到自主列车运行控制系统分析图； 基于所述自主列车运行控制系统分析图对所述自主列车运行控制系统进行非形 式化描述； 基于所述非形式化描述对所述自主列车运行控制系统进行建模； 采用Event ‑B形式化方法对所述自主列车运行控制系统的模型进行优化； 通过Rodin平台中的定理证明器对优化后的自主列车运行控制系统的模型进行证 明。 [0006]可选地， 所述自主列车运行控制系统包括列车、 区段资源和资源管理器； 在所述自说　明　书 1/8 页 3 CN 115494829 A 3