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

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.