基于通信的列车控制系统中控制参数计算的在线验证

基于通信的列车控制（CBTC）系统是最先进的列车控制系统。在CBTC系统中，为保证列车运行安全，列车之间进行密集通信，并根据获取的信息自主计算关键控制参数（例如速度范围）来调整其控制模式。由于生成的控制参数的正确性对系统安全至关重要，因此验证这些参数的方法在列车控制领域有着强烈的需求。在本文中，我们提出了如何高效地对CBTC系统中的控制参数计算进行建模和验证的思路。 - 由于系统的行为高度非确定性，预先在线构建和验证系统的完整行为空间模型是困难的。因此，我们建议根据由控制参数引发的持续行为模型来对系统进行建模。 - 由于参数是在线生成并快速更新的，如果验证结果超出时间限制，则验证结果将毫无意义，因为届时模型已经改变。因此，我们提出了一种方法，用于在线快速验证模型中是否存在某些危险场景。为了证明这些提出方法的可行性，我们提出了带有可读共享变量的组合线性混合自动机作为建模语言，对控制参数计算进行建模，并给出了一种面向路径的可达性分析技术，用于该模型的基于场景的验证。我们展示了为CBTC系统构建的模型，并展示了我们的技术在快速在线验证中的性能。最后，由于CBTC系统是一个典型的CPS系统，本文还简要讨论了CPS验证的潜在方向。