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

Hierarchical Safety Requirement Modeling and Validation Method for Interlocking Systems Based on STPA

摘要

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

Abstract

To address the issues of insufficient dynamic behavior modeling and weak traceability of hierarchical constraints in the safety requirement verification of railway interlocking systems, a safety requirement modeling and validation method based on the synergy of System-Theoretic Process Analysis (STPA) and formal development is proposed. First, an extended STPA framework is established to create a multi-level safety requirement model, refining abstract system-level safety constraints at the top into specific safety requirements. Second, a hierarchical refinement strategy tailored for the railway interlocking system is designed to systematically transform safety requirements into invariants and event guard conditions of formal models. Finally, a formal verification tool chain is introduced, integrating a hybrid verification mechanism combining theorem proving, model checking, and behavior simulation. Theorem proving verifies each refinement level, model checking explores state spaces and generates counterexamples to comprehensively validate the correctness of model invariants and Linear Temporal Logic (LTL) properties derived from safety requirements, and simulation reproduces typical operational scenarios to confirm the system is deadlock-free and meets expected safety requirements. The results show that through 3 hierarchical refinements, 132 proof obligations are decomposed across 4 model layers, and the safety requirements are further validated using formal verification tools. This process effectively reduces the complexity of safety requirement modeling for railway interlocking systems, and lays a solid foundation for their safe operation.

Graphical abstract

关键词

铁路联锁系统 / 形式化方法 / 安全需求 / 线性时序逻辑 / STPA

Key words

Railway interlocking systems / Formal method / Safety requirements / Linear Temporal Logic (LTL) / System-Theoretic Process Analysis (STPA)

联锁系统作为现代轨道交通信号控制的核心，在保障列车运行安全和提升运输效率方面具有不可替代的作用^［1］。该系统通过实时监测轨道占用、动态控制道岔和信号机显示，构建列车进路和运行间隔的防护体系。然而，随着铁路向智能化、网络化发展，传统联锁系统面临多重挑战：一方面，电气化改造与自动化升级使系统组件间交互复杂度急剧上升；另一方面，基于故障树分析和失效模式与影响分析的传统安全分析方法在应对非线性系统行为、多重故障耦合及人机交互、环境扰动与软件控制联动等复杂场景时，逐渐显现出理论局限，可能造成系统性风险识别盲区。

欧洲铁路安全标准EN 50129（CENELEC，2018）明确要求对安全相关电子系统实施全生命周期风险管理^［2］。该标准强调通过系统化方法识别危险源与推导安全需求，并对SIL3级及以上系统推荐采用形式化开发技术以确保设计规范与安全需求的数学可证明性。传统危害识别方法难以应对现代信号控制要求：故障树分析的静态失效概率难以描述动态状态迁移，失效模式与影响分析的组件级分析无法有效捕捉跨子系统交互的级联效应^［3］。因此，探索符合EN 50129的新型安全工程方法体系成为铁路信号安全领域亟须突破的关键问题。

在此背景下，由Leveson提出的基于系统理论过程分析（Systems Theoretic Process Analysis，STPA）的安全工程方法展现出独特的理论优势，该方法突破传统可靠性工程的“组件失效”分析范式，从控制论视角解构复杂系统的安全约束^［4］。通过分层控制结构模型，系统性识别可能导致危险状态的“不安全控制行为”，尤其适用于分析人机协同、软件控制逻辑与物理设备间的动态交互风险。研究表明，STPA在航空电子、核电控制等安全苛求系统的应用中，已成功识别出传统方法遗漏的潜在危险场景^［5］。然而，现有文献针对铁路联锁系统的STPA应用研究多集中于安全约束识别与分析层面，在如何将STPA生成的多层级安全需求与形式化开发过程深度融合方面，尚无标准化实施路径^［6］。

在形式化开发领域，基于Event-B形式化方法的精化策略，通过协调定理证明、模型检验和行为仿真，为安全需求的形式化验证与确认提供创新性解决方案。Event-B通过抽象机和精化机制构建分层模型体系，其核心优势体现在：首先，基于数学规约的高层模型能够表达系统抽象的功能和安全需求；其次，通过逐层精化，逐步融入物理设备行为及控制逻辑时序等实现细节，形成从需求到设计的可追溯链路^［7］。借助Event-B开发平台Rodin的Atelier B和ProB组件，可完成定理证明、模型检验与行为仿真，动态验证和确认STPA生成的安全需求^［8］。

针对联锁系统的特性，提出1种基于STPA-Event-B-ProB的3阶段验证框架，适用于从抽象到具体的各层模型验证：第1阶段，通过STPA建立分层安全需求模型，将系统级安全约束分解为组件级的安全需求；第2阶段，构建控制结构到Event-B模型的映射，将各层安全需求转化为该模型中的不变式与事件守卫条件，实现功能和安全需求层级对齐及Event-B规约，并在Rodin平台完成定理证明^［9］；第3阶段，利用ProB工具对安全需求进行逐层确认，实现不同抽象层级需求的可视化确认与交互式调试，通过将安全需求转化为线性时序逻辑（LTL）进行模型检测和仿真，确保系统不违反安全需求和不存在死锁，且系统行为符合预期，通过定理证明、LTL检测和仿真的混合验证策略，形成了符合EN 50129标准的安全证据链。

1 联锁系统

铁路联锁系统通过安全控制道岔的扳动和信号机的显示确保行车安全。基于进路的联锁系统以进路作为资源管理的逻辑单位，安全高效地预留和释放资源，预留进路涉及锁定资源供单列列车使用，而进路释放则是在使用或取消后解除资源锁定，联锁系统与自动列车监控系统（ATS）协作，处理进路请求和取消，确保多列列车安全共存^［10］。

1.1　预留与取消进路

对于ATS的预留进路请求，联锁系统需周期性检测区段状态，确保安全的预留进路。具体操作包括：预留相关区段、切换道岔至指定位置并锁定，将信号机设为绿灯表示进路可用^［11］。进路预留和释放示意图如图1所示。图中：R1和R3为进路；B2和B3为需预留的区段；P1为道岔；SG01和SG07为信号机；T1和T2均为列车。将P1扳动至反位并锁闭，将SG07设为绿灯，表示进路可用。

当ATS发送取消进路请求时，若进路尚未被占用，联锁系统将通过进路控制器取消已经预留的相关进路。具体操作包括：先将信号机转为红色，禁止列车进入该进路；再取消该进路预留的所有区段（若为有岔区段，则需解锁道岔）。当进路控制器R1收到取消请求后，会将SG07设为红色，解锁道岔P1，并取消区段B2和B3的预留。

1.2　顺序释放区段

当列车驶入进路后，控制器会根据区段占用状态释放区段：若该区段为有岔区段，则先解锁道岔再释放区段；若为无岔区段，则直接释放区段。当所有区段均被释放后，进路重新开放供ATS系统接收新请求。

例如，列车T1占用R3时，控制器随列车通过B2，B3和B4逐步释放各区段，释放B3前需解锁P1，最终进入B4，R3释放B2和B3后，控制器可以预留B2和B3建立进路R1。这种顺序释放机制可有效提升资源共享效率。

2 方法概述

复杂联锁系统的安全分析与设计是1项具有挑战性的任务，核心在于保障安全需求的一致性和正确性。所提方法融合了STPA安全分析和基于Event-B的形式化建模，能够系统性地识别、规约和验证系统的安全需求。该方法从明确分析目的出发，通过逐步精化控制结构和过程模型变量，分层识别不安全控制行为并生成安全需求，利用Event-B逐层对系统功能和安全需求进行形式化规约和验证，最终结合具体场景数据确认安全需求。通过分解与迭代分析，能够有效降低复杂系统的建模与验证难度，确保安全性设计的全面性与可靠性。安全验证框架如图2所示。

2.1　确定分析目的

在系统安全分析的初始阶段，明确分析目的至关重要，需遵循清晰且逻辑递进的流程。首先，定义系统级事故，为后续步骤提供明确的目标指向。其次，根据系统级事故识别系统中潜在的危害，并对其进行科学分类。在此基础上，依据识别结果制定系统级安全约束，划定后续安全性分析的边界与目标。这一阶段的核心目标是为整个分析过程构建理论框架和实践指导，确保后续步骤围绕系统安全的核心需求有序展开。

2.2　精化控制结构和过程模型变量

在明确系统危害并确立安全约束后，进一步构建系统的抽象控制结构并进行逐层精化，以有效应对系统的复杂性。精化次数主要由控制结构的控制器嵌套层数决定，每个精化阶段对应1个或1层控制器的展开，确保系统功能的增量分析、规约和验证。在初始模型中，控制器被视为黑盒，被控过程也抽象为控制目标，以形成较高抽象层级的控制结构，从而实现层次化规约和验证。

精化过程从抽象的控制器及其被控对象出发，逐步引入更具体的被控对象和对应的控制器，同时定义控制命令和反馈机制，构建完整的控制回路。此外，随着控制结构逐步细化，还需细化过程模型变量，以动态反映被控对象及其环境的状态。通过对控制结构和过程模型变量的分层精化，为STPA提供结构化基础，形成层级化安全需求为形式化规约的制定创造条件，可有效降低分析、规约和验证的复杂性^［12］。

2.3　STPA推导安全需求

在构建或精化控制结构后，需对控制结构中新出现的控制命令进行分析，以识别潜在的不安全控制动作。控制命令的安全性与其对应控制器的过程模型变量取值相关，需综合评估以下场景进行分析：控制命令在特定情境下提供、不提供、过早或过晚提供是否会造成危害。所提分步精化方法首先针对初始进路控制器的命令进行分析，随后在每次精化后，对新引入的控制命令进行迭代评估，推导出对应不同抽象层级控制模型的安全需求。

通过系统化的评估可全面审视控制命令在多种运行情境下的潜在影响，识别可能导致系统事故的不当控制，并据此制定切实可行的安全需求。从抽象到具体的分析路径，与前述控制结构的精化过程紧密衔接，体现了分析逻辑的连贯性和递进性。

2.4　建立Event-B模型

本步骤以前期控制结构精化与STPA迭代所得的分层安全需求为基础，构建初始Event-B模型，并逐步精化该模型以支持系统性的增量验证与确认。在初始Event-B模型中，将控制结构中的控制行为、过程模型变量及STPA得出的安全需求纳入规约范围。具体而言，进路控制器的控制行为被抽象为Event-B机器中的事件（Event），过程模型变量被映射为Event-B的变量或常量，安全需求则转化为事件中的守卫条件（Guard）。此外，与初始模型相关的系统级安全约束转化为不变式，以验证安全需求。

随着控制结构和过程模型的精化，Event-B模型同步更新：新引入控制器的控制命令和过程模型变量按照与初始模型类似的方式进行规约，细化模型涉及的新的系统级安全约束也转换为不变式。通过分层精化，Event-B模型随着控制结构的逐步细化而不断完善，以数学化的方法精确描述系统特性，确保系统设计从抽象的高层逐步过渡到具体的实现细节，确认功能需求和安全需求的一致性，并评估STPA识别的安全需求是否充分满足系统级安全约束^［13］。

2.5　确认安全需求

2.4节中提出将安全需求表示为Guard、系统级安全约束表示为不变式，实现联锁系统通用安全逻辑的静态形式化验证。然而，联锁系统的安全性还与具体车站站场的配置数据相关，需结合实际站场数据，通过模型检测和行为仿真进一步确认系统是否满足安全需求。首先，基于站场数据对初始Event-B模型进行实例化，并将初始安全需求转化为与站场数据相关的LTL表达式；随后，利用Rodin平台上的ProB工具进行LTL模型检测和行为仿真。若系统违反安全需求，ProB工具将生成反例，据此对模型进行调整优化。若系统通过所有安全需求检测，则进一步通过仿真分析，模拟系统运行状态，确认其在各种场景下的行为表现^［14］。

随着Event-B模型精化，站场数据实例化过程同步更新，针对不同抽象层级安全需求构建LTL表达式，并迭代进行LTL模型检测及仿真分析，根据反例持续优化模型。

3 案例分析

3.1　确定分析目的

建立清晰的系统级安全约束条件是联锁系统开发的初始环节，这些约束通过对系统事故演变的分析得出，其逻辑为自上而下的映射关系：由事故推导危险源，再由危险源决定安全约束。编号A对应系统事故、H对应危险源、SC对应安全约束，以此实现全生命周期的信息可追溯管理和安全要素管理。联锁系统事故类型见表1，前3种均属于列车碰撞事故，第4种为脱轨事故。

表2展示了基于系统事故推导的系统级危害及其关联关系，每起系统事故至少对应1个系统级危险定义，单个危险源可能触发多类事故。列车追尾发生于列车驶入已经被另一同向列车占用的区段，可归因于危险源H-1至H-5。正面碰撞源自列车驶入对向列车的区段，可由危险源H-2至H-5引发。侧面碰撞可由道岔错误操作引发，可追溯至危险源H-2至H-5。列车脱轨可能因为道岔转换或道岔固定在错误位置时驶入进路，归咎于危险源H-3至H-5。

基于已识别的危险转化而来的系统级安全约束见表3。SC-1通过禁止列车驶入已占用的进路规避H-1风险；SC-2通过限制进路控制器预留冲突进路，消除H-2的潜在危害；SC-3通过整合H-3与H-4的要求，确保进路预留后全线道岔锁闭在正确位置；SC-4针对H-5制定，禁止释放/取消已被列车占用的进路，避免中途强制释放/取消进路引发的危险。

3.2　初始模型建立及验证过程

3.2.1　系统理论过程分析

本阶段旨在构建抽象系统控制结构，并通过STPA分析得到安全需求，作为后续开发的基础框架。初始控制结构如图3所示，控制结构通过实线箭头（控制命令）和虚线箭头（状态反馈）构建闭环交互系统，明确各实体的功能边界与责任。

列车接近轨道网络时，列车自动监控系统将根据运行计划，向联锁系统发送“进路预留”命令，提前锁定行进路径。必要时可发出“进路取消”命令，请求取消已预留的进路。进路控制器负责接收ATS的进路预留/取消请求，并对其进行响应，在确保安全的情况下进行进路锁定和进路释放操作。在控制命令的执行层面，列车在接收到相应指令后完成具体的移动：执行“驶入”命令进入已成功预留的进路；在进路保持期间，根据“前进”指令沿预定路径行进；抵达进路末端或指定位置时执行“驶离”命令，离开当前进路。

进路控制器的初始过程模型变量及对应取值见表4。当进路控制器接收到ATS的预留进路请求时，变量Route Mode取值为Req（请求），表示当前处于请求处理状态；当ATS发出取消进路请求时，该变量取值为Can（取消）；若无任何请求接收，则变量值为Free（空闲）。对于变量Path Mode，取值为Free表示该路径尚未被控制器预留，而Res则标识该路径已被成功预留。对于变量Path State，在列车未驶入进路前标记为Free，列车驶入后更新为Occ（占用），列车驶离后则变更为Uoc（解除占用）。当进路控制器未预留冲突路径时，变量No Conflicting Paths Res取值为Yes，否则取值为No。

结合层级功能控制结构中的动态控制行为与控制器的过程模型，对其进行STPA分析，可能引发风险的不安全控制行为（UCAs）^［15］见表5。进而提出以下安全需求（SR）以缓解这些控制行为的潜在风险^［16］。

SR-1：若V4取值为No，禁止预留进路。

SR-2：若V3取值为Occ，禁止取消进路。

SR-3：若V3取值为Occ，禁止释放进路。

3.2.2　初始Event-B模型

为构建初始Event-B模型，创建名为SR0_PATH的上下文，对控制结构进行形式化规约。引入2个基本类型ROUTE和PATH，分别表示进路与路径的有限集合。定义常量PathConflict为PATH间的二元关系，表示2条路径间的冲突关系；公理PathConflict=PathConflict~表示冲突关系是对称的；常量InitPath为初始路径，InitPath⊆PATH表示初始路径为路径的子集；常量Route2InitPath将进路映射至其初始路径，由公理Route2InitPath∈ROUTE→InitPath进行定义；常量SubPath表示2条路径间的子路径关系；常量NullPath∈PATH，表示长度为0的路径。

初始模型SR_M0通过变量Route_Req和Route_Cel分别表示Route Mode中的Req与Can状态，两者均受不变式约束，为ROUTE的子集。变量Route_Occ与Path State相关联，当某路径状态为Occ时，预留了该路径的进路在Route_Occ集合中，并由不变式Route_Occ⊆ROUTE约束。变量Route2Path构建进路与其预留路径的映射关系，当一条路径的Path Mode值为Res时，其对应的进路位于Route2Path的定义域内。冲突检测机制则通过变量No Conflicting Paths Res实现，当路径冲突集合PathConflict［Route2Path［｛r1｝］］中的路径未被其他控制器预留时，该变量值为Yes，否则值为No。模型通过变量间的动态关联与不变式约束，严格实现过程模型变量的状态转换逻辑^［17］。

为满足系统级安全约束，将SC-2和SC-4转换为Event-B模型中的不变式。

inv1：∀r1，r2 · （r1≠r2∧r1∈dom（Route2Path）∧r2∈dom（Route2Path））⇒（PathConflict~［Route2Path［｛r1｝］］∩Route2Path［｛r2｝］=∅）

inv2：∀r · r∈Route_Occ⇒（Route2Path［｛r｝］≠∅）

初始形式化模型包含8个事件，与开发的初始控制结构所定义的8个控制动作相对应，分别由ATS系统、进路控制器和列车触发。此外，模型还包含1个INITIAL（初始化）事件，用于为模型变量设置初始值。初始模型中引入的事件见表6。为确保系统满足安全需求，需将安全需求转化为相应事件的守卫条件（Guard），仅当某个事件的所有Guard满足时，才允许执行该事件。以预留进路事件为例，执行该事件需要满足该进路处于请求模式、不处于取消模式且路径处于空闲模式。在此基础上，还需加入由安全需求SR-1转化而来的特定守卫条件（在模型中标记为grd4），其内容是确保待预留路径与已预留路径均无冲突。仅当上述所有条件均满足时，事件才能执行，从而完成对该进路初始路径的预留。该事件的Event-B代码示例如下。

Route_Reserve

ANY r

WHERE

grd1：r∈Route_Req∧r ∉ Route_Cel

grd2：r∉dom（Route2Path）

grd3：PathConflict［Route2InitPath［｛r｝］］∩ran（Route2Path）=∅

THEN

act1：Route2Path≔Route2Path∪｛r↦Route2InitPath（r）｝

END

为确保模型的逻辑正确性，在Rodin平台上为每层模型生成相应的证明义务。通过形式化证明严格验证事件执行后系统的状态不会违反不变式。在初始模型中，通过完成证明义务保证不会预留冲突的路径且进路被占用时不会被取消。

3.2.3　安全需求确认

在对联锁系统Event-B模型进行仿真时，需要将轨道网络布局实例化为模型中的常量和集合，并将其定义为公理^［18］，轨道网络布局如图4所示。该布局中包含R1和R2两条进路，P11和P12等10条路径；R1的初始路径为P13，R2的初始路径为P23；路径之间有重叠即说明2条路径之间是冲突的；子路径（SubPath）关系刻画了随着列车前进，原路径逐渐缩短为更短路径的过程，如P12为P13的子路径。

根据3.2.1中得到的安全需求，构建相应的LTL表达式进行模型检测，其中SR-1表达式如下。

F（｛Route2Path（R2）∈PathConflict~［Route2Path［｛R1｝］］｝⇒｛¬（R2∈dom（Route2Path）∧R1∈dom（Route2Path））｝）

对以上LTL表达式进行检测，结果未发现反例，说明模型符合安全需求。根据实例化结果进行仿真分析，以预留进路R1和列车在该进路上的前进过程为例，事件按顺序执行后，变量Route2Path的变化过程见表7。预留进路时，先预留R1的初始路径P13，随着列车前进，预留的路径逐渐缩短，直至预留的路径为空，并在列车驶离之后，释放进路。

3.3　第1次模型精化

3.3.1　系统理论过程分析

在确认初始模型符合安全约束后，该过程将对控制结构进行精化，加入更低层次的区段控制器，第一次精化的控制结构如图5所示，其功能与职责为：按进路控制器命令，单独预留各区段；按进路控制器命令，单独取消各区段；按进路控制器命令，根据列车已经通过且不再占用的顺序，依次释放各区段。

进路控制器的过程模型也需精化，原有变量Path State被精化为No Blocks Are Occ（无区段被占用），若原变量值为Occ，则新变量值为No，表示路径被占用。原变量No Conflicting Paths Res被精化为No Blocks Are Res（无区段被预留），若原变量值为Yes，则新变量值也为Yes。引入的新变量All Blocks Are Res表示初始进路的完整预留状态，进路控制器成功预留构成初始进路的所有区段时，值为Yes。变量Track Block Mode表示区段的预留状态：当某区段被预留时，该变量值为Res。变量Track Block State表示区段的物理占用状态：当区段空闲时，变量值为Free；当区段被列车占用时，变量值为Occ；当列车完全通过且不再占用时，变量值为Uoc。第1次精化过程中模型所有变量及其取值见表8。

基于第1次精化控制结构的动态控制行为及过程模型，将进路层面的安全需求展开至区段层面，STPA构建类似于3.2.1的不安全控制行为表，得到不安全控制行为UCA-4至UCA-11，并推导出对应安全需求SR-4至SR-11。

SR-4：若V4=No，禁止预留进路。

3.3.2　第1次精化Event-B模型

基于更精确的控制结构和过程模型，对Event-B模型进行同步精化。将上下文精化为SR1_BLOCK，引入BLOCK表示区段的有限集合。对路径及其相关结构做出如下定义：常量Path2Block及公理Path2Block∈PATH→\mathbb{P}（BLOCK）表示每条路径对应的区段集合；常量Head和Rear表示路径的第1个和最后1个区段；常量Next表示路径中区段顺序；常量OneBlockPath表示仅有1个区段的路径，并通过公理OneBlockPath⊆PATH表示其为PATH集合的子集；常量SubPath用于表示2条路径间的子路径关系，由不变式SubPath∈PATH⇸PATH表示。

精化的模型SR_M1定义了3个新变量，其中：变量Route2OccPath为进路中占用的路径，当占用的路径为NullPath或进路不在该变量定义域中时，No Blocks Are Occ值为Yes，由不变式Route2OccPath∈ROUTE⇸PATH表示；变量Block2Route为进路中预留的区段，由不变式Block2Route∈BLOCK⇸ROUTE表示，进路的初始路径对应的所有区段均不在Block2Route的定义域时，No Blocks Are Res值为Yes，进路的初始路径对应的所有区段均在Block2Route的定义域时，All Blocks Are Res值为Yes，某个区段在Block2Route定义域内时，Track Block Mode值为Res；变量Block2OccRoute为进路中占用的区段，当区段属于该变量定义域时，Track Block State值为Occ，当区段属于Block2Route的定义域但不属于Block2OccRoute的定义域时，Track Block State值为Free，当区段属于Block2Route的定义域但不属于Route2Path的定义域时，其值为Uoc。

为在区段层面重新解释初始模型中的不变式inv1和inv2，将进路的安全需求分层展开至区段层面，并保持前后精化层次之间的语义一致性。添加黏合不变式inv3和inv4：若2条路径冲突等价于其对应区段集合的交集非空，且当某条进路被预留时，则该进路所包含的所有区段也相应被预留。

inv3：∀p，q · p∈PATH∧q∈PATH∧q∈PathConflict［｛p｝］⇔（（Path2Block（p）∩Path2Block（q））≠∅）

inv4：∀r · r∈dom（Route2Path）∧Route2Path（r）≠NullPath∧r∉Route_Cel⇒Block2Route~［｛r｝］≠∅

此外，第1次精化模型新增事件见表9。在预留进路事件中，为满足安全需求SR-5，即进路中所有区段均被预留才能预留进路，将此安全需求转化为Guard并新增了grd5。

grd5：Block2Route~［｛r｝］=Path2Block（Route2InitPath（r））

3.3.3　安全需求确认

在精化模型中，需要实例化常量和集合。网络布局中共包含A，B，C和D四个区段，P11，P21，P14和P24为仅包含1个区段的路径，路径P13对应的区段集合为｛A，B，C｝，区段顺序表示为A↦B，B↦C，SubPath描述列车前进方向逐渐延伸的路径之间的子路径关系，例如，图4中的P15是P13的子路径。以安全需求SR-4为例，将其转换为LTL进行模型检测，表达式如下。

G （｛Block2Route~［｛R1｝］≠Path2Block（Route2InitPath（R1））｝⇒｛Route2Path≠Route-2Path∪｛R1↦Route2InitPath（R1）｝∨R1∈Route_Cel｝）

根据实例化结果进行仿真分析，列车在进路R1前进过程中，变量Block2OccRoute的变化过程见表10。随着列车前进，逐步占用区段A，B和C，随后列车在尾前进的过程中，不再占用的区段顺序释放，直至占用的区段为空，最后释放进路。

3.4　第2次模型精化

3.4.1　系统理论过程分析

第2次精化控制结构如图6所示，在控制结构加入道岔控制器，其功能与职责为：按进路控制器命令，扳动道岔；按进路控制器命令，解锁或锁闭道岔。

过程模型同步精化，新增变量见表11。当进路中所有道岔处于正确位置时，变量All Points Aligned（所有道岔正确对齐）值为Yes；当道岔均锁闭时，变量All Points Locked（所有道岔锁闭）值为Yes。变量Point Position和Point Mode表示单个道岔位置和锁闭状态，Point Position值为Ali时表示道岔已对齐，Point Mode值为Loc时表示道岔锁闭。

基于第2次精化控制结构的动态控制行为及过程模型，得到不安全控制行为UCA-12至UCA-20，推导出对应安全需求SR-12至SR-20，其中SR-19和SR-20为

SR-19：若V8取值为No，禁止预留进路。

SR-20：若V9取值为No，禁止预留进路。

3.4.2　第2次精化Event-B模型

在精化的上下文SR2_Point中，引入2个有限集合POS和MODE，分别表示道岔位置和锁闭状态，POS包含正位（Plus）和反位（Minus）2个元素，MODE包含锁闭（Lock）和未锁闭（Unlock）2个元素。常量POINT表示道岔，为区段的子集；由公理Point2InitPos∈POINT→POS定义常量Point2InitPos，表示道岔的初始位置；由公理Route2Point2Pos∈（ROUTE↔POINT）⇸POS定义常量Route2Point2Pos，表示进路中道岔的正确位置。

在精化的模型机器SR_M2中引入2个变量，其中Point2Pos表示道岔位置，Point2Mode表示道岔模式（锁闭状态）。当某道岔在进路中的位置与常量 Route2Point2Pos 所定义的位置一致时，变量Point Position的值为Ali；若该道岔锁闭，变量Point2Mode值为Loc；若进路中所有道岔位置都与Route2Point2Pos表示的道岔位置相同，则变量All Points Aligned的值为Yes；若所有道岔均锁闭，变量All Points Locked值为Yes。

为满足SC-3安全约束并保持前后精化层次之间的语义一致性，引入黏合不变式inv5，表示进路和区段被预留后道岔应处于正确位置并锁闭。

inv5：∀po · （∀p · p∈ran（Route2Path）∧po∈（POINT∩Path2Block（p）））⇒Point2Mode（po）=Lock

此外，第2次精化模型新增事件见表12。在预留进路事件中，需要满足安全需求SR-19和SR-20，即所有道岔均处于正确位置并锁闭。

3.4.3　安全需求确认

在第2次精化模型中，对常量进行实例化处理。区段B为道岔区段，初始位置为反位，在进路R1中应处于正位，R2中应处于反位。以安全需求SR-19为例，将其转换为以下LTL表达式，表示若进路中存在道岔未处于正确位置，则不能预留进路。

G （｛∀po · po∈Block2Route~［｛R1｝］∩ POINT∧Point2Pos（po）≠Route2Point2Pos（｛R1↦po｝）｝⇒F｛¬（R∈dom（Route2Path））｝）

根据实例化结果进行仿真分析，列车在驶入进路前，变量Point2Pos（道岔位置）和Point2Mode（道岔模式）的变化过程见表13，道岔区段B初始在反位，且未锁闭，将其扳动至正位并锁闭后，才能预留进路R1。

3.5　第3次模型精化

3.5.1　系统理论过程分析

该精化步骤中，在控制结构中加入信号机控制器，如图7所示，其功能与职责为根据进路控制器的命令将信号机切换为红灯或绿灯。信号机控制器的过程模型包含Signal State（信号机状态），编号为V12，变量值包含绿灯（Green）和红灯（Red），Green表示列车可以驶入进路，Red则禁止驶入。

基于第3次精化控制结构的控制命令及过程模型，由STPA得到UCA-21至UCA-33，对应生成SR-21至SR-33，其中SR-21为

SR-21：若V3取值为No且V12取值为Red，禁止提供绿灯。

3.5.2　第3次精化Event-B模型

在精化的上下文SR3-Signal中引入1个SIGNAL集合，并定义常量 Green 和 Red 作为该集合的2个元素。在精化的模型SR_M3中引入变量Route2Signal，表示每个进路的信号机状态，其与过程模型变量取值相对应。将安全约束SC-1体现为黏合不变式inv6，表示一旦列车占用进路，信号机须为红灯，后续列车禁止驶入。

inv6：∀r · r∈dom（Route2OccPath）∧Route2OccPath（r）≠NullPath⇒Route2Signal（r）=Red

3.5.3　安全需求确认

在第3次精化模型中，对SIGNAL集合进行实例化处理。以安全需求SR-21为例，进路中道岔未被全部预留时，不能切换为Green，将其转换为LTL表达式。

G （｛Block2Route~［｛R1｝］≠Path2Block（Route2InitPath （R1））｝⇒F｛¬（Route2Signal（R1）=Green）｝）

根据实例化结果进行仿真分析，以预留进路R1和列车驶入进路后的过程为例，事件执行后，变量Route2Signal的变化过程见表14。信号机默认为Red，预留进路之后切换为Green，并在列车驶入后切换为Red。

4 试验结果及分析

为保证各层语义的一致性，在每一精化层中添加黏合不变式，建立抽象模型和具体模型之间的映射关系，并生成相应的证明义务，通过完成所有的证明义务严格保证模型在逻辑上的正确性。各层模型中证明义务数量统计结果见表15。由表15可知，经过3次精化，模型中共132条证明义务分解至4层模型中，将复杂的系统级安全约束分层展开至不同层次的安全需求中，复杂逻辑分解为模块化层级，每层生成少量且更简单的证明义务，降低了验证复杂性^［19］。

通过结合ProB动态仿真和LTL检测，可发现静态证明义务验证过程中的遗漏问题。例如，在初次建模中，以公理形式定义了路径自身无冲突的性质；在第1次精化过程中，通过引入不变式将路径间无冲突等价于区段无交集，并顺利完成Event-B模型的证明义务验证，从表面上确认了“路径自身不存在冲突”的正确性。但将轨道网络实例化进行ProB仿真时，工具检测到模型实际上违反了所设定的公理，其根源在于路径自身的区段在实际场景中存在交集。因此，取消了路径自身之间无冲突的预设定义，从而确保理论验证和实际行为的一致性。在初次建模中，定义子路径之间为二元关系，在TrainRearMove事件的1个Guard中，原定义sp∈PathSub［｛p｝］，因初始路径包含多条子路径，导致ProB仿真时无法准确确定sp的值。因此，优化了子路径定义，确保仿真结果的准确性。

在完成上述2条进路的轨道网络仿真后，为验证该方法的可扩展性，对包含10条进路的大型轨道网络布局进行ProB仿真和LTL模型检测。结果表明，即便在规模与复杂性提升的情况下，该模型依然能够稳健运行，且所有安全属性在形式化验证均得到严格保持，未发现任何安全约束冲突或逻辑死锁，充分满足了系统安全需求。这表明该方法不仅适用于中小规模的联锁系统，也能够有效扩展至复杂的大型铁路场景，为后续复杂交通控制系统的安全建模与验证提供了可行的技术路径与方法支撑。

5 结语

本研究提出1种融合Event-B和STPA的铁路联锁系统开发与安全需求建模及确认方法。该方法通过整合形式化建模的严谨性与STPA的系统安全分析能力，能够对STPA所识别的安全需求进行精确的建模与验证，确保联锁系统可有效避免列车碰撞等严重事故的发生^［20］。为应对建模过程中可能出现的复杂性问题，采用分层精化的策略，将安全需求的建模与验证任务分解为多个阶段，从高层次的系统级安全约束出发，逐步细化为组件级的安全需求^［21］。借助ProB工具链的支持，模型在每一精化层级上都能够进行仿真和LTL模型检测，以此确认系统的安全需求。

通过ProB的状态空间探索和反例生成功能，结合数学证明和仿真分析，可对每层模型的安全性进行迭代检查与优化。这种动态仿真与静态验证相结合的双重验证机制，能够发现Event-B模型可能遗漏的问题，从而对模型进行迭代优化。所提层次化的形式化建模方法为联锁系统的开发提供了1种结构化、高效且可靠的技术路径，既降低了开发过程中的复杂性，又为系统的安全运行奠定了基础。

基于本研究构建的理论框架，后续研究可从多个维度进行深化。具体而言，未来的工作可聚焦于：如何将STPA得到的安全需求和系统级安全约束自动转化为Event-B形式化规约；如何将形式化模型高效转换为可执行的计算机程序代码；如何实现图形化仿真以提升验证直观性。通过在这些方向上的持续探索，将有望形成1套从安全分析、形式化验证到代码生成与仿真验证的完整、闭环的联锁系统开发方法。

参考文献

[1] HERNANDO A， GALÁN-GARCÍA J L， AGUILERA-VENEGAS G. A Fast and General Algebraic Approach to Railway Interlocking System across All Train Stations ［J］. AIMS Mathematics， 2024， 9 （3）： 7673-7710.

[2] OKOH P， DONG H S， LIU Y. Cross-Acceptance of Fire Safety Systems Based on SIL Equivalence in Relation to IEC 61508 and EN 50129 ［J］. Safety and Reliability， 2022， 41 （2）： 103-120.

[3] ABDULKHALEQ A， WAGNER S， LEVESON N. A Comprehensive Safety Engineering Approach for Software-Intensive Systems Based on STPA ［J］. Procedia Engineering， 2015， 128： 2-11.

[4] LEVESON N G. Extending the Human Controller Methodology in Systems-Theoretic Process Analysis （STPA） ［D］. Cambridge： Massachusetts Institute of Technology， 2014.

[5] LEVESON N G， THOMAS J P. STPA Handbook ［M］. Cambridge： MIT PSASS， 2018.

[6] LA N T， KWON G. Risk Assessment for STPA with FMEA Technique ［C］// International Conference on Frontier Computing. Singapore： Springer， 2019： 444-455.

[7] SALEHI FATHABADI A， SNOOK C， DGHAYM D， et al. Designing Critical Systems Using Hierarchical STPA and Event-B ［C］// International Conference on Rigorous State-Based Methods. Cham： Springer， 2023： 220-237.

[8] RIVIERE P， SINGH N K， AÏT-AMEUR Y， et al. Formalising Liveness Properties in Event-B with the Reflexive EB4EB Framework ［C］// NASA Formal Methods Symposium. Cham： Springer， 2023： 312-331.

[9] YAR A. An xDSL-Based Framework for Validation of Railway Models： Application to ERTMS/ETCS and EULYNX ［D］. France： Grenoble Alpes University， 2023.

[10] 郭弘倩，南迪.基于云架构的城市轨道交通信号系统方案研究［J］.铁路通信信号工程技术，2024，21（2）：72-77，102.

[11] GUO Hongqian， Di NAN. Research on Urban Rail Transit Signal System Scheme Based on Cloud Architecture ［J］. Railway Signalling & Communication Engineering， 2024， 21 （2）： 72-77， 102. in Chinese

[12] 黎晨光.城市轨道交通全电子计算机联锁系统的应用研究［D］.北京：中国铁道科学研究院，2022.

[13] LI Chenguang. Application Research on All-Electronic Computer Interlocking System in Urban Rail Transit ［D］. Beijing： China Academy of Railway Sciences， 2022. in Chinese

[14] TSUJI M， TAKAI T， KAKIMOTO K， et al. Prioritizing Scenarios Based on STAMP/STPA Using Statistical Model Checking ［C］// 2020 IEEE International Conference on Software Testing， Verification and Validation Workshops （ICSTW）. New York： IEEE Press， 2020： 124-132.

[15] MAMMAR A， FRAPPIER M， TUENO FOTSO S J， et al. A Formal Refinement-Based Analysis of the Hybrid ERTMS/ETCS Level 3 Standard ［J］. International Journal on Software Tools for Technology Transfer， 2020， 22： 333-347.

[16] HAXTHAUSEN A E， FANTECHI A. Compositional Verification of Railway Interlocking Systems ［J］. Formal Aspects of Computing， 2023， 35 （1）： 1-46.

[17] CHEN Z， NIU C， MEI M， et al. Hierarchical Safety Analysis and Formal Verification for Safety-Critical Systems Using STAMP and Event-B ［J］. Safety Science， 2025， 184： 106744.

[18] ABDULKHALEQ A， WAGNER S. Integrated Safety Analysis Using Systems-Theoretic Process Analysis and Software Model Checking ［C］// International Conference on Computer Safety， Reliability， and Security. Cham： Springer， 2015： 121-134.

[19] HOANG T S， SNOOK C， DGHAYM D， et al. Class-Diagrams for Abstract Data Types ［C］// International Colloquium on Theoretical Aspects of Computing-ICTAC 2017. Cham： Springer， 2017： 100-117.

[20] LEUSCHEL M， Modelling NAYERI N.， Visualisation and Proof of an ETCS Level 3 Moving Block System ［C］// International Conference on Reliability， Safety， and Security of Railway Systems. Modelling， Analysis， Verification， and Certification. Cham： Springer， 2023： 193-210.

[21] FÜRST A. Formal Development of a Train Control System Using Event-B ［D］. Swiss： ETH Zurich， 2015.

[22] KWON R， KWON G. Formal Verification of STPA with Model Checking ［J］. Scientific Journal of Gdynia Maritime University， 2023 （125）： 7-24.

[23] 陈祖希，牛传军，梅萌，等.基于Event-B与ADT的TACS形式化开发方法与验证［J］.中国铁道科学，2023，44（6）：172-183.

[24] CHEN Zuxi， NIU Chuanjun， MEI Meng， et al. Formal Development Method and Verification of TACS Based on Event-B and ADT ［J］. China Railway Science， 2023， 44 （6）： 172-183. in Chinese

基金资助

国家重点研发计划项目(2022YFB4300504)

国家铁路局研究计划课题(KF2024-039)