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

Research on Contract Relationship between Balise Data and Vehicle System Based on CPTA

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

Line data are basic to the train operation safety. The present researches of train control data focus too much on the integrity and validity verification of data themselves, but focus little on the contract relationship between data and the host system, which may ignore the hazards caused by the failure of data to meet the needs of the host system. To address the above issue, syntax, semantics and timeliness requirements needed by the process that the ATP system calculates the dynamic monitoring curve were extracted, and then formalized as the PVS axioms to act as the train state migration conditions to construct the contract model based on CPTA. Finally, the contract model was verified to be correct by means of sequent calculus of PVS. The results show that, the balise packet can be verified efficiently and reliably based on the proposed contract model between balise and vehicle, which can reduce the number of abnormal braking or speed reduction resulting from the balise data failures.