08A 安全关键系统的建模与验证

01October2026第2单元安全关键系统的建模与验证kmwang@王恪铭Fromsystemspecificationverificationtosystemspecificationdesign从系统规范验证到系统规范设计案例：使用Event-B的铁路平交道口管理系统铁路事故的主要原因是什么?脱轨事故？碰撞？动机Keming

Wang,

Zheng

Wang基于Event-B的铁路平交道口管理系统的建模与验证一、系统规范验证

其他人轨道车辆火灾碰撞运行中的轨道车辆脱轨事故平交道口2016年欧盟28国按事故类型和人员类别划分的伤亡人数来源：欧盟统计局（在线数据代码：tran_sf_railvi）被杀死受伤动机2014年欧盟成员国共有108196个平交道口。欧盟平均每10公里线路不到五个平交道口。在欧盟，2015年LC事故占所有铁路事故的26%（469/1808），占38.6%（264/684）的伤害和30.7%（296/963）的伤亡。2016年，该项目占28.3%（220/778）的伤亡和26.6%（256/964）的伤亡。来源：欧盟铁路机构研究综述梁等人开发了铁路平交道事故预测模型（2018年）；Ghazel等人分析了不同类型LC设备的可靠性（2014）;Mekki等人验证了一种新的平交道装置（2012年）。……影响液相保护安全的因素还包LC管理及其保护装置等。LC管理系统的研发基于管理规范。

平交道规范中可能存在的缺陷和误解，这些都可能影响系统的可靠性。要求规格该系统有两个基本的安全规范：SAF1：列车通过LC时，LC应关闭。SAF2：列车离开LC后，LC可以重新开放铁路LC管理系统功能规范分析▶单线轨道自动保护装置的系统铁路LC管理系统LC系统的基本事件流程基本事件的iUML图机器文件(Machine_0)Machine_1VariableInvariantEventEventguardaction机器文件(Machine_0)Context_1CarrierSetConstantAxiomNotTheory模型的精炼过程使用Event-B的原型模型精炼步骤物品与活动第二次精炼引入考勤钟，并为开门和关门事件添加时间限制。第三次精炼引入火车、信号灯等物体，并添加火车接近、火车靠近、火车驶离道口以及信号灯变化等事件。第四次精炼再加上列车接近事件的时间限制、关闭时间。INV1：系统收到列车接近信息后，LC应在必要时间内打开，以便LC清空。系统功能验证Event-Bdescriptionofsystemfeatures时间该系统的当前时间Time_Approach_GateClosing

LC的时间结束T_TrainApproach

列车发送接近信息的瞬间Train_Information

表示列车接近LC时当前状态的变量

INV1INV2：列车将在发送接近信息后的特定时间内发送关闭信息。INV3：系统下令关闭门后，应在设定时间内关闭门。

INV2

INV3T1包括LC清理和大门关闭Time_Closing

门关闭的设置时间T_ClosingStart

交付成交命令的时刻系统功能验证系统功能验证INV4：列车发送关闭信息后，列车将在一定时间内通过LC。INV5:当列车接近LC时，LC也应关闭。T_TrainClose

关闭消息发送的那一刻Time_Closing_Coming

列车关闭与离开LC之间的最长T2时间。

INV4

INV5系统功能验证系统特征的事件B描述INV6：LC必须等列车离开LC后才能打开。INV7：系统发出开门命令后，门应在设定时间内打开。T_OpeningStart

下达开盘命令的时刻Time_Opening

大门开启的时间设定

INV6

INV7系统功能验证系统特征的事件B描述●我们假设接近的列车可以实时获得LC状态。然而，当前的LC管理系统没有此功能。LC管理系统的改进在上述流程中，我们修订原型模型，并发现规格中的缺陷，即列车无法实时获得LC状态。真实时间传输至接近列车LC状态现在是否状态异常？

LC状态YN火车正在刹车列车继续向LC行驶LC管理系统的改进信用证异常时的处理流程INV8：当LC状态异常时，系统应向接近列车发送制动警告。Crossing_Infor

LC状态的变量TrainOrder列车运行命令的变量INV8

结论与未来工作形式化模型和验证有助于发现和纠正系统规范中潜在的设计漏洞，以及开发可靠的编码阶段基础原型。（WR