基于时间自动机的CBI道岔转换时间建模与验证

针对CBTC计算机联锁安全性十分重要的问题，介绍时间自动机理论，分析CBTC计算机联锁系统的结构和与传统联锁系统的区别，以CBTC联锁系统的道岔转换功能为例，采用UPPAAL建立了道岔转换模型，分析模型的安全需求。表明了在联锁系统开发过程中采用基于时间自动机建模与验证的方法的可行性和有效性。

Modeling and verification of CBI switch transaction time based on timed automata

Focusing on the problem that the safety of CBTC computer based interlocking is critical, this article introduced the theory of timed automata, analyzed the architecture and differences between CBTC computer based interlocking system and traditional interlocking system, took an example of switch transaction, switch transaction model was established by using UPPAAL. The security requirements of the model were also analyzed, which showed the feasibility and effectiveness of the modeling and verification methods based on timed automata, during the process of developing computer based interlocking system.