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

Safety Design of Level Crossing Control System Based on Formal Method

作　　者：王霞[1,2] 王恪铭[1,2] 徐扬[2,3] 唐伟健 WANG Xia;WANG Keming;XU Yang;TANG Weijian(School of Computing and Artificial Intelligence,Southwest Jiaotong University,Chengdu 610031,China;National-Local Joint Engineering Laboratory of System Credibility Automatic Verification,Southwest Jiaotong University,Chengdu 610031,China;School of Mathematics,Southwest Jiaotong University,Chengdu 610031,China;School of Information Science and Technology,Southwest Jiaotong University,Chengdu 610031,China)

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

出　　处：《西南交通大学学报》2023年第1期109-116,共8页Journal of Southwest Jiaotong University

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

摘　　要：铁路平交道口控制系统是一种典型的安全苛求系统,为提高铁路平交道口的安全性,提出一个能适应双线双向接车的自动控制系统.首先,分析现有铁路平交道口的作业流程,利用新的控制系统解决现有系统中常见的三个问题,即出清检查、制动距离限制、连续接车中防护门短时间开放问题;其次,基于Event-B语言以及精化策略对设计的自动控制系统建立形式化模型;最后,检查证明义务以验证需求属性是否被满足,并应用动画器Animation展示系统功能的正确性.结果显示:相比传统的道口管理系统,本文提出的自动控制系统增加了双线连续接车功能,且使用形式化建模和验证,避免系统设计中存在的二义性,对平交道口安全管理有一定的参考意义.Railway level crossing(RLC)control system is a typical safety-critical system.A novel automatic control system(ACS)that responds to a two-track bi-direction operation is proposed to improve the safety of RLC.Firstly,the operational processes at traditional railway level crossings is analyzed,and the corresponding solutions are proposed in the ACS for three general problems,i.e.,clearing inspection,braking distance limitation,and short-time opening of the barriers during continuous work.Secondly,a formal model based on the Event-B language and refinement strategy are developed for the proposed ACS.Finally,proof obligations are checked to verify that the required properties are satisfied,and the Animation is applied to demonstrate the correctness of the system functionality.The results reveal that,compared with the traditional level-crossing management system,the proposed ACS adds the function of two tracks of continuous work,and the use of formal modeling and verification avoids the ambiguity in the system design,all of which have reference significance for RLC safety management.

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

分 类 号：TP301.1[自动化与计算机技术—计算机系统结构] U284.3[自动化与计算机技术—计算机科学与技术]