列车安全距离控制形式化建模与验证
开篇：润墨网以专业的文秘视角，为您筛选了一篇列车安全距离控制形式化建模与验证范文，如需获取更多写作素材，在线客服老师一对一协助。欢迎您的阅读与分享！
摘要：随着我国铁路的迅速发展，对列车运行安全性的要求越来越高。采用EventB形式化建模方法研究了高速列车安全距离控制形式化验证问题，以EventB形式化仿真工具Rodin为基础，通过结合多智能体理论，引入感知决策法则，实现了无线闭塞中心（RBC）与列车的车地通信，建立了多列车运行的安全距离控制模型。仿真研究了高速列车最小间隔追踪控制运行，对列车安全距离控车行为进行了形式化建模并进行了POs证明义务验证。仿真结果表明，对于CTCS列车控制系统的复杂逻辑关联行为，采用提出的EventB和多智能体系统（MAS）结合的形式化验证方法，可进行系统规范的模型验证，对于复杂系统的逻辑验证有较强的实际意义。
关键词：EventB方法；列车控制；多智能体；形式化建模；分布式系统
中图分类号： TP301.2
文献标志码：A
Abstract： With the rapid development of Chinese railway， requirements for running safety of trains are more high. This paper used the EventB formal modeling approach to research on the highspeed train safety distance control. With the support of simulation tool Rodin， combined with the multiAgent theory， the safety distance control model of multitrain operation was constructed. The simulation researched the modeling and verification on the minimum interval tracking control for high speed train. The simulation results show that， the binding of formal verification methods of EventB and MultiAgent System （MAS） is meaningful. So the method has some practical significance for the modeling and verification of complex system.
Key words： EventB method； train control； multiAgent； formal modeling； distributed system
0引言
近年来，我国铁路发展迅速，列车的速度不断提高，列车的运营间隔不断地缩短，加之最近发生多起列车追尾事故，这就使列车之间安全的行车距离的问题凸显出来，对列车安全距离控制问题的研究显得尤为重要。
铁路安全是永恒的主题，针对铁路安全的问题国内外学者做了许多研究，其中比较流行的方法是用形式化建模并验证来保证复杂系统的安全。形式化方法在数学、计算机科学、人工智能等领域得到广泛运用，它能精确地揭示各种逻辑规律，制定相应的逻辑规则，使各种理论体系更加严密，通常用于开发注重安全性的高度整合的系统。吕继东等[1]提出一种时间自动机对无线闭塞中心（Radio Block Center， RBC）子系统进行形式化建模，应用UPPAAL验证工具验证RBC的安全性；陈永等[2]用细胞膜计算方法对列车无线通信机制模型进行了形式化建模并进行了数值分析；张友兵等[3]用有色Petri网对RBC切换进行了形式化建模并验证，得出消息重发时间间隔和RBC重叠范围会影响车载设备进行RBC切换的成功概率的结果；赵林等[4]利用UML对列控系统特性进行了形式化建模与分析验证。但是以上的模型均侧重于对研究问题模型性能的验证与分析，对模型本身形式化验证较少，模型自身是否存在逻辑错误并没有进行过多演算和证明，而EventB基于传统的谓词演算和定理证明，因此它非常适合用来为周期行为建模；另外，EventB还支持逐步精化地建立系统模型，用户可以在建模之初构建一个粗略的原型，然后不断地使用精化策略，增量开发能够极大地减少漏洞的出现[5]。本文拟采用EventB与多智能体系统（MultiAgent System， MAS）相结合的形式化验证方法，研究多列车安全距离控制问题，对列车的安全运行并且保证旅客的切身利益有一定的现实意义。
1EventB形式化方法
在EventB模型[6-8]中，每一个MACHINE都有唯一的概括性的名称，VARIABLES条目里面的变量值都有自己的范围，INVARIANT不变式里面都定义了变量和它们的安全特性的状态空间。EVENTS条目里包括一系列事件，每个事件都定义了其发生的条件WHERE和满足条件后发生的动作THEN，并且EVENTS都用INITIALISATION来初始化每个EVENT。CONTEXT用来定义静态变量和集合。
每个MACHINE至少参考（sees）一个CONTEXT，证明义务（Proof Obligations， POs）用来确保MACHINE的一致性，如图1所示。
参考文献：
[1]LYU J， TANG T， JIA H. Modeling and verification of radio block center of CTCS3 train control system for dedicated passengers lines[J].Journal of the China Railway Society，2010，32（6）：34-42.（吕继东，唐涛，贾昊.客运专线CTCS3级列控系统无线闭塞中心的建模与验证[J].铁道学报，2010，32（6）：34-42.）
[2]CHEN Y， WANG X， DANG J， et al. Research on a novel membrane computing method based on biochemistry reaction rate and its application [J]. Journal of the China Railway Society， 2011， 33（10）： 61-66.（陈永，王晓明，党建武，等.一种基于生化反应速率的新型膜计算方法研究与应用[J].铁道学报，2011，33（10）：61-66.）
[3]ZHANG Y， TANG T. The modeling and formal analysis of RBC handover for CTCS3 train control system based on colored Petri nets [J]. Journal of the China Railway Society， 2012， 34（7）： 49-55.（张友兵，唐涛.基于有色Petri网的CTCS3级列控系统RBC切换的建模与形式化分析[J].铁道学报，2012，34（7）：49-55.）
[4]ZHAO L， TANG T， LIU J， et al. Research on train control systems modeling method using UML extensibility mechanisms [J]. Journal of the China Railway Society， 2012， 34（12）： 64-70.（赵林，唐涛，刘金涛，等.基于UML扩展机制的列控系统建模方法研究[J].铁道学报，2012，34（12）：64-70.）
[5]QI Y， SHEN H， CHEN Z， et al. EventB interpretation for space aircraft description language model [J]. Journal of Computer Applications， 2012， 32（12）： 3525-3528.（綦艳霞，沈慧丽，陈朝晖，等.SPARDL模型的EventB解释[J].计算机应用，2012，32（12）：3525-3528.）
[6]RAGHURAJ S， DIVAKAR Y. Modeling of multiversion concurrency control system using EventB [C]// Proceedings of the 2012 Federated Conference on Computer Science and Information Systems. Piscataway， NJ： IEEE Press， 2012： 1397-1401.
[7]LORINA N， IRINA M， ADINA M F. Formal specification and verification of concurrent Agents in EventB [C]// Proceedings of the 19th International Conference on Control Systems and Computer Science. Piscataway， NJ： IEEE Press， 2013： 155-161.
[8]MOHAMED T， MOHAMED M， DOMINIQUE M. From eventB specifications to programs for distributed algorithms [C]// Workshops on Enabling Technologies： Infrastructure for Collaborative Enterprises. Piscataway， NJ： IEEE Press， 2013： 104-109.
[9]ZHAO H， LIU T. Research on vehicle dispatching at container terminal based on multiple Agent system [J]. Computer Engineering and Applications， 2010， 46（21）： 246-248.（赵辉，刘铁男.MAS理论下集卡动态调度系统研究[J].计算机工程与应用，2010，46（21）：246-248.）
[10]LIN Y， WANG C. Computational model of safe braking curve of onboard ATP based on CBTC [J]. Journal of the China Railway Society， 2011， 33（8）： 69-72.（林颖，王长林.基于CBTC的车载ATP安全制动曲线计算模型研究[J].铁道学报，2011，33（8）：69-72.）
[11]SHANGGUANG W， CAI B， WANG J， et al. Braking mode curve arithmetic of highspeed train above 250km・h-1 [J]. Journal of Traffic and Transportation Engineering， 2011， 11（3）： 41-46.（上官伟，蔡伯根，王晶晶，等.时速250km以上高速列车制度模式曲线算法[J].交通运输工程学报，2011，11（3）：41-46.）
[12]PEREVERZEVA I， TROUBITSYNA E， LAIBINIS L. Formal development of critical multiAgent systems： a refinement approach [C]// Proceedings of the 9th European Dependable Computing Conference. Piscataway， NJ： IEEE Press， 2012： 156-161.
[13]TRUONG NT， TRINH TB， NGUYEN VH. Coordinated consensus analysis of multiAgent systems using eventB [C]// SEFM09： Proceedings of the 2009 Seventh IEEE International Conference on Software Engineering and Formal Methods. Piscataway， NJ： IEEE Press， 2009： 201-209.