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

摘要：

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

关键词：车地协同;联锁子系统;形式化方法;HCPN;状态空间分析

所属期刊栏目：19

分类号：U284.3(铁路通信、信号)

资助基金：国家自然科学基金61661027

在线出版日期：2022-03-03（万方平台首次上网日期，不代表论文的发表时间）

页数：共11页

页码：52-62