进路联锁系统安全需求推导与形式化验证方法

打开文本图片集

中图分类号：TP399 文献标志码：A 文章编号： 1000-5013（2026）02-0136-10

Abstract：Based on the ever-growing intelligent requirements and security verification challenges of railway interlocking systems，a safety analysis framework that integrates system-theoretic process analysis （STPA） with Kind2 model checking is proposed. First，STPA is employed to systematically elicit safety requirements. Then，the requirements are translated into formal invariants and verified using the Kind2 model. The experimental results on a simulated station yard dataset show that all17 safety requirement invariants are determined to be Valid within the unfolding depth of k=2 ， with no counterexample traces generated. The proposed safety verification method combining STPA and formal model checking can efectively identify complex interaction risks that are often overlooked by traditional analysis methods， while providing stronger safety guarantees through formal verification. This framework further enhance the reusabilityand robustness of interlocking system in intelligent railway operation scenarios.

Keywords：railway interlocking system;system-theoretic process analysis （（STPA）；artificial intellgence; Kind2 model；formal verification method

铁路联锁系统是保障行车安全的核心防护设施，负责在特定战场拓扑内协同多个控制器执行逻辑防护，从而防止碰撞、脱轨或路径冲突[1-6]。（剩余13423字）