道口管理系统多参数的形式化建模与验证

Formal Modeling and Verification of Multi-parameter Model of Level Crossing Management System

铁路平交道口作为铁路安全的瓶颈,其作业流程的缺陷是导致安全事故发生的重要原因之一。而现有道口管理规范大部分只针对单线接车,对于双线双向接车没有给出详细的规范。为了丰富实际流程,基于道口管理规范,探讨双线双向道口连续接车的问题,同时考虑道口接车作业流程中存在的异常,提出流程方案。分析系统环境属性、功能属性和安全属性,并利用UPPAAL时间自动机进行建模仿真,对模型的属性进行验证,根据验证结果确认方案流程的可行性。结果表明,本文所提出的多参数道口作业流程更符合实际情况,改进了多列车接车流程,并提出了接车过程中异常情况下的应对方案。

As the bottleneck of railway security,the defect of railway level crossing(LC)operation is one of the important reasons leading to safety accidents.Most of the existing LC specifications are only for the single-track,but not for dual_track LC.This paper discussed the problems of the continuous connection at the LC and the abnormal situation in the process,then presented a detailed scheme in order to enrich the actual environment.We considered the environment properties,function properties and safety properties based on UPPAAL,model and simulation are carried out to verify the properties of the model,and the feasibility of the scheme flow is determined according to the verification results.The results shown the multi-parameter LC operation process presents in this paper is satisfied with the actual situation,improves the process of the multi-train,and purposes the measure to solve the abnormal situations during the process.