离散事件系统仿真 课件 08A 安全关键系统的建模与验证、08B 多智能体建模验证

第2单元安全关键系统的建模与验证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

结论与未来工作形式化模型和验证有助于发现和纠正系统规范中潜在的设计漏洞，以及开发可靠的编码阶段基础原型。（WRSPM模型，杰克逊和扎韦）这正是系统中任何假设的本质！未来的研究将考虑多列车双轨的环境，基于物联网技术设计并验证物流管理系统的新原型。ThanksSouthwestJiaotongUniversity多代理建模与验证可信决策——列车运行管理局案例为什么？列车控制系统做出的不安全运行决策如何规范控制系统的决策行为？2023年6月印度铁路事故241.当前的不足系统需求的缺陷决策条件不完备逻辑变量变更过程对控制决策过程的影响。——它容易在系统设计中出现缺陷，导致作风险和巨大的缺陷修正成本。252.安全关键决策的可信性质。探索可信决策过程的定义，并提出可信决策的属性。介绍了感测变量的演化规则以及计算树逻辑定义的性质公式，并基于模型检查的可信决策过程。提出在正式建模和验证下，制定列车移动权威的新决策流程。263.1可信决策的定义确保条件变量正确感知场景中的对象，并充分考虑决策场景中的相关条件。273.1可信决策的定义定义1：安全关键系统中的可信决策定义2:可信决策过程的关键因素定义3:关键因素的同源变量283.2可信决策属性引理1:决策条件的充分性引理2:系统变换的一致性293.2可信的决策制定特性引理3:动作执行过程中的一致性保持引理4:可信决策的及时性304.1可信决策的制衡表计算树逻辑（CTL）用于检验我们为可信决策过程提出的属性。F1-决策条件充分性公式F2-系统转换的一致性公式……314.1检查可信决策的制定情况F3-执行动作的一致性公式F4-决策及时性公式。324.2变量的演变与可信的决策过程建立系统模型并实现决策属性验证的关键在于如何表达决策变量的演化过程。根据系统元素的感知值，被监测对象的状态被表示为二进制值，决策变量仅有正常和异常两种状态。334.2变量的演变与可信的决策过程模型中过于简单化的演化规则以及状态间变化的无序表达在模型内表达状态的复杂度显著增加有效地缩小了模型的状态尺度，同时支持属性检查。344.2变量的演变与可信的决策过程基于上述决策可信度和模型演化规则的性质公式，我们提出了一种针对安全关键系统的新型决策流程。355.1为新型MA原型建模本文的案例将MA过程与交叉层面场景相结合，把整个交叉路段视为一个区块，并考虑了具有已知影响因素的MA决策过程。可信移动授权（TMA）的可信决策过程可分为三个阶段：决策推理决策行动准备MA的行动执行365.1新型MA原型的建模决策过程的状态机图375.1为新型MA原型建模我们使用了模型检查器MCMAS（多智能体系统模型检查）进行建模，它支持基于认知逻辑和CTL的规范说明。MCMAS模型中包含两种类型的智能体：标准智能体和环境智能体，每个智能体由以下部分组成：一组局部状态一组动作一个协议（一条描述智能体在特定局部状态下可以执行哪些动作的规则）一个演化函数（描述智能体的局部状态如何根据其当前局部状态和其他智能体的动作发生演化）385.1为新的MA原型建模TMA决策代理的ISPL代码运用层级逻辑来判断决策条件。395.1对新型MA原型进行建模传感器检测代理的ISPL代码405.1对新型MA原型进行建模用于决策变量功能状态评估代理的ISPL代码415.1为新的MA原型建模在验证模型之前，我们在评估模块中为公式验证定义布尔变量。425.1为新型MA原型建模一个能自动生成相应的传感器代理和功能评估代理的应用程序435.2可信属性验证为了验证该模型决策条件的充分性、一致性及其时效性，我们在该模型上验证了9个CTL公式。关于引理1：决策条件的充分性公式1：如果生成了TMA，那么参与上一次TMA评估的所有受影响变量均正常。公式2：如果无法生成TMA，那么上一次TMA评估的正常决策变量数量小于规定的影响变量数量。关于引理2：系统转换的一致性公式3：它验证了不同传感模式下每个决策变量的逻辑一致性。445.2可信属性验证关于引理3：动作执行过程中的一致性保持公式4：当TMA维持生成状态时，相关决策变量在决策行动执行前需要保持一致。否则，TMA状态无法维持。关于引理4：可信决策的及时性公式5：它验证TMA生成或不生成的状态会根据实时决策评估发生变化。公式6-9：它们验证了四个决策变量状态的实时可变性455.2可信属性验证MCMAS中带有验证结果的CTL公式465.2可信属性验证不同模型进化规则的效果比较模型验证的执行时间大约增加了1237.5%（即13.375倍），而模型状态的数量大约增加了84%。此外，内存使用量大约增加了15.8%，并且出现了属性检查公式失败的情况。这表明改进演化规则既必要又合理