车地协同下的联锁子系统HCPN建模与验证

• 作者: 王兴 李茂青 岳丽丽 王耀东
• 来源期刊: 铁道科学与工程学报
• 学科: 交通运输
• 关键词: 车地协同 联锁子系统 形式化方法 HCPN 状态空间分析
• 年，卷（期）: 2022,（1）
• 所属期刊栏目: 智慧交通与物流|Intelligent Transportation and Logistics
• 页码范围: 52-62
• 页数: 11页
• 分类号: U284.3
• 语种: 中文
• DOI: 10.19713/j.cnki.43-1423/u.T20210092

摘要

联锁子系统作为站内行车安全的关键保障,是车地协同下的列车运行控制系统的重要组成部分.传统联锁子系统存在地面集中控制失效风险大、列车自主化程度低等不足,为顺应精简系统结构、降低运营成本和提升列车自主化的列控技术发展趋势,设计一种车地协同下的联锁子系统用于城际铁路.考虑多车间的进路冲突是影响子系统功能实现的关键因素,提出进路预延伸策略以避免列车间的进路冲突.为确保联锁子系统功能安全,采用一种基于层次着色Petri网(HCPN)的系统功能建模与验证方法.通过对联锁子系统的主要功能实现过程—进路建立过程进行分析,提取子系统的功能需求,以此建立顶层需求模型.为缩小底层实现与顶层需求之间的差距,建立基于数据及行为低抽象度表达的模块层模型,并在其中引入死锁控制策略实现对系统功能逻辑的完整表达.以冲突进路建立场景为模型的输入参数,执行验证过程,通过对模型标准状态空间性能分析,实现对模型正确性的检验.在此基础上,采用分支时序逻辑ASK-CTL公式与状态空间搜索算法相结合的验证方法,完成对子系统功能安全性的检验.研究结果表明:模型的行为特性同子系统预期相一致,能够正确表达系统的行为.所设计子系统满足功能安全需求,可为底层实现提供依据.