列车安全距离控制形式化建模与验证

《列车安全距离控制形式化建模与验证》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、列车安全距离控制形式化建模与验证摘要：随着我国铁路的迅速发展，对列车运行安全性的要求越来越高。采用EventB形式化建模方法研究了高速列车安全距离控制形式化验证问题，以EventB形式化仿真工具Rodin为基础，通过结合多智能体理论，引入感知决策法则，实现了无线闭塞中心（RBC）与列车的车地通信，建立了多列车运行的安全距离控制模型。仿真研究了高速列车最小间隔追踪控制运行，对列车安全距离控车行为进行了形式化建模并进行了POs证明义务验证。仿真结果表明，对于CTCS列车控制系统的复杂逻辑关联行为，采用提出的Event

2、B和多智能体系统（MAS）结合的形式化验证方法，可进行系统规范的模型验证，对于复杂系统的逻辑验证有较强的实际意义。关键词：EventB方法；列车控制；多智能体；形式化建模；分布式系统分类号：TP301.2文献标志码：AAbstract：WiththerapiddevelopmentofChineserailway,requirementsforrunningsafetyoftrainsaremorehigh.ThispaperusedtheEventBformalmodelingapproachtoresearc

3、honthehighspeedtrainsafetydistancecontrol.WiththesupportofsimulationtoolRodin,combinedwiththemultiAgenttheory,thesafetydistancecontrolmodelofmultitrainoperationwasconstructed.Thesimulationresearchedthemodelingandverificationontheminimumintervaltrackingcontrol

4、forhighspeedtrain.Thesimulationresultsshowthat,thebindingofformalverificationmethodsofEventBandMultiAgentSystem(MAS)ismeaningful.Sothemethodhassomepracticalsignificanceforthemodelingandverificationofcomplexsystem.Keywords:EventBmethod；traincontrol；multiAgent；

5、formalmodeling；distributedsystem0引言近年来，我国铁路发展迅速，列车的速度不断提高，列车的运营间隔不断地缩短，加之最近发生多起列车追尾事故，这就使列车之间安全的行车距离的问题凸显出来，对列车安全距离控制问题的研究显得尤为重要。铁路安全是永恒的主题，针对铁路安全的问题国内外学者做了许多研究，其中比较流行的方法是用形式化建模并验证来保证复杂系统的安全。形式化方法在数学、计算机科学、人工智能等领域得到广泛运用，它能精确地揭示各种逻辑规律，制定相应的逻辑规则，使各种理论体系更加严密，通常用

6、于开发注重安全性的高度整合的系统。吕继东等［1］提出一种时间自动机对无线闭塞中心(RadioBlockCenter,RBC)子系统进行形式化建模，应用UPPAAL验证工具验证RBC的安全性；陈永等［2］用细胞膜计算方法对列车无线通信机制模型进行了形式化建模并进行了数值分析；张友兵等［3］用有色Petri网对RBC切换进行了形式化建模并验证，得出消息重发时间间隔和RBC重叠范围会影响车载设备进行RBC切换的成功概率的结果；赵林等［4］利用UML对列控系统特性进行了形式化建模与分析验证。但是以上的模型均侧重于对研究问

7、题模型性能的验证与分析，对模型本身形式化验证较少，模型自身是否存在逻辑错误并没有进行过多演算和证明，而EventB基于传统的谓词演算和定理证明，因此它非常适合用来为周期行为建模；另外，EventB还支持逐步精化地建立系统模型，用户可以在建模之初构建一个粗略的原型，然后不断地使用精化策略，增量开发能够极大地减少漏洞的出现［5］。本文拟采用EventB与多智能体系统(MultiAgentSystem,MAS)相结合的形式化验证方法，研究多列车安全距离控制问题，对列车的安全运行并且保证旅客的切身利益有一定的现实意义。l

8、EventB形式化方法在EventB模型［6_8］中，每一个MACHINE都有唯一的概括性的名称，VARIABLES条目里面的变量值都有自己的范INVARIANT不变式里面都定义了变量和它们的安全特性的状态空间。EVENTS条目里包括一系列事件，每个事件都定义了其发生的条件WHERE和满足条件后发生的动作THEN,并且EVENTS都用INITIALISATION来初始化每