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

摘要：

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

关键词：报文数据、车载、契约关系、概率时间自动机

所属期刊栏目：41

分类号：U283(铁路通信、信号)

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

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

页数：共9页

页码：102-110