华侨大学学报（自然科学版）2026，Vol.47Issue(2)：136-145,10.DOI:10.11830/ISSN.1000-5013.202511005
进路联锁系统安全需求推导与形式化验证方法
Security Requirement Derivation and Formal Verification Method for Route Interlocking System
摘要
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 experi-mental results on a simulated station yard dataset show that all 17 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 effectively 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 reusability and robustness of interlocking sys-tem in intelligent railway operation scenarios.关键词
轨道交通联锁系统/系统理论过程分析(STPA)/人工智能/Kind2模型检查/形式化方法Key words
railway interlocking system/system-theoretic process analysis(STPA)/artificial intelligence/Kind2 model/formal verification method分类
信息技术与安全科学引用本文复制引用
张世旭,陈祖希,梅萌,潘亮,汪小勇..进路联锁系统安全需求推导与形式化验证方法[J].华侨大学学报（自然科学版）,2026,47(2):136-145,10.基金项目
国家铁路局研究计划项目(KF2024-039) （KF2024-039）
