基于CPTA实现报文数据与车载系统契约关系的研究

• 作者: 唐涛 王彤典
• 来源期刊: 铁道学报
• 学科: 交通运输
• 关键词: 报文数据 车载 契约关系 概率时间自动机
• 年，卷（期）: 2019,（4）
• 所属期刊栏目: 铁道通信信号、信息化
• 页码范围: 102-110
• 页数: 9页
• 分类号: U283
• 字数: 7136字
• 语种: 中文
• DOI: 10.3969/j.issn.1001-8360.2019.04.014

摘要

线路数据是驱动列控系统安全运行的基础.目前,有关列控数据安全的研究多集中于验证数据自身的完整性与合理性,却很少关注数据与其宿主系统间的契约关系,这可能会忽视由于数据没有满足宿主系统需求而产生的安全隐患.针对此问题,分析车载ATP在计算动态监控曲线过程中对报文语法、语义和时效性三方面的需求,并将其形式化为PVS公理,作为列车状态迁移条件来构建报文-车载CPTA契约模型,借助PVS定理证明工具证明该契约模型的正确性.实验结果表明,基于报文-车载的契约模型能够实现高效且可靠的报文验证,从而减少由于报文数据失效而引发的列车异常制动或降速的次数.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	唐涛	北京交通大学轨道交通控制与安全国家重点实验室	152	2578	27.0	40.0
2	王彤典	北京交通大学轨道交通控制与安全国家重点实验室	3	8	1.0	2.0