基于交互式马尔可夫链的列车运行控制系统安全通信实时性的研究

The data processing time would cause safety communication latency in the train control system, and it is difficult to judge the real-time performance of the system. But even worse, it is not conducive to system safety, also affects the efficiency. The premise of the present study is too idealistic, and not in accordance with the actual existence. This project is based on the real-time model optimization and model checking algorithm to research on the real-time for safety communication in train control system. Firstly, with the kronecker operator based MTBDDs, an improved algorithm is presented to increase the regularity of the variable order in the Interactive Markov Chains model checking, and to construct the generator matrix of synchronization command sets in the systems. The algorithm is proposed to deal with the state space explosion of the Interactive Markov Chains model. Secondly, adaptation of preconditioned GMRES algorithm, the ill-conditioning of matrix has been reduced and the convergence of Interactive Markov Chains model checking has been improved. Thirdly, a timeliness judging algorithm is proposed, which lays a foundation on the construction of the model checking tool to automatic verification of the train control system. This research can provide theoretical support for determining the timeliness of safety communication in train control system.

列车运行控制系统的安全通信过程中由于信道传输和数据处理而产生延时，为系统实时性判定带来困难，不利于系统安全，也影响运营效率。目前该问题研究前提假设过于理想化，与实际存在偏差。本项目拟从系统实时性模型优化和模型检验算法入手，对列车运行控制系统安全通信实时性进行研究。首先，针对系统安全通信的交互式马尔可夫链模型，基于多终端二叉判决图(MTBDDs)，结合Kronecker算子，优化交互式马尔可夫链模型检验状态变量排序的规则性，改进系统Kronecker算子的同步状态转换生成矩阵的产生，解决模型中状态空间爆炸问题；然后，利用稀疏矩阵的预条件GMRES迭代算法，解决交互式马尔可夫链模型的可靠性分析中病态矩阵问题，提高模型检验的稳定性和收敛速度。最后，给出系统安全通信实时性判定算法，为今后开发系统的模型检验平台奠定基础。该研究能为系统安全通信的实时性判定提供理论支持。

列控系统是一个复杂的安全苛求系统，通信的实时性是保证系统可靠和安全的重要因素。本项目融合了传统马尔可夫链和标记迁移系统，构建基于交互式马尔可夫链模型，对列控系统安全通信的实时性进行了深入研究。主要研究了列车运行控制系统安全通信的交互式马尔可夫链模型的表达和构建，解决了带有同步和并发现象的实现问题。针对建立的模型，提出了基于穷举式的迭代算法进行模型求解和验证，目标是判定模型是否满足所给的状态公式。项目综合了现有的列控系统安全通信中存在的各类延时和随机因素，提出了一种用于判定信息时效性的算法。用定理证明的方法证明了算法的正确性，通过长时间测试和分析，验证了算法具有较高的可靠性。由于列控系统安全通信网络的实时性包含了多个节点之间数据传输，其延时时间界限不易获得，因此对比并总结了仿真、排队论以及网络微积分等其它方法在该方面的应用。项目还基于网络演算理论对列控系统安全通信网络的实时性判定算法进行了多场景仿真，旨在分析和评价算法的实时性和可靠性，为系统的设计和优化提供依据。相关的研究成果不仅可以为我国自主研发和设计列控系统安全通信协议提供依据，也有助于标准协议的制定与性能改善。