基于STPA的联锁系统层级安全需求建模及确认方法OA

针对铁路联锁系统安全需求验证中存在的动态行为建模不足和层级约束可追溯性弱等问题,提出1种基于系统理论过程分析(STPA)与形式化开发协同的安全需求建模及确认方法。首先,通过扩展STPA框架,建立多层次的安全需求模型,将顶层抽象的系统级安全约束逐步精化为具体的安全需求;其次,设计面向铁路联锁领域的分层精化策略,实现安全需求向形式化模型不变式与事件守卫条件的系统性转化;最后,引入形式化验证工具链,构建集定理证明、模型检测和行为仿真于一体的混合验证机制,通过数学证明完成各精化层级的验证,利用模型检验的状态空间探索与反例生成功能,全面验证由安全需求转化而来的模型不变式及线性时序逻辑(LTL)的正确性,并通过仿真复现典型运行场景,确认系统无死锁且满足预期的安全需求。结果表明:经过3次分层精化,将132条证明义务分解到4层模型中,并通过形式化验证工具进一步完成安全需求的确认,有效降低了铁路联锁系统安全需求建模的复杂性,也为铁路联锁系统的安全运行奠定了基础。