基于形式化方法的平交道口控制系统安全设计

作     者：王霞 王恪铭 徐扬 唐伟健 WANG Xia;WANG Keming;XU Yang;TANG Weijian

作者机构：西南交通大学计算机与人工智能学院四川成都610031 西南交通大学系统可信性验证国家地方联合工程实验室四川成都610031 西南交通大学数学学院四川成都610031 西南交通大学信息科学与技术学院四川成都610031 

出 版 物：《西南交通大学学报》 (Journal of Southwest Jiaotong University)

年 卷 期：2023年第58卷第1期

页      面：109-116页

核心收录：

学科分类：08[工学] 0837[工学-安全科学与工程] 0835[工学-软件工程] 082302[工学-交通信息工程及控制] 0811[工学-控制科学与工程] 0823[工学-交通运输工程] 0812[工学-计算机科学与技术（可授工学、理学学位）] 081202[工学-计算机软件与理论] 

基　　金：国家自然科学基金(61976130,61673320) 四川省科技计划(2022NSFSC0464)。 

主　　题：平交道口 控制系统 需求规范 安全苛求系统 形式化方法 

摘      要：铁路平交道口控制系统是一种典型的安全苛求系统,为提高铁路平交道口的安全性,提出一个能适应双线双向接车的自动控制系统.首先,分析现有铁路平交道口的作业流程,利用新的控制系统解决现有系统中常见的三个问题,即出清检查、制动距离限制、连续接车中防护门短时间开放问题;其次,基于Event-B语言以及精化策略对设计的自动控制系统建立形式化模型;最后,检查证明义务以验证需求属性是否被满足,并应用动画器Animation展示系统功能的正确性.结果显示:相比传统的道口管理系统,本文提出的自动控制系统增加了双线连续接车功能,且使用形式化建模和验证,避免系统设计中存在的二义性,对平交道口安全管理有一定的参考意义.