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

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

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

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

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

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

页      码：109-116页

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

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

学科分类：08[工学] 0837[0837] 0835[0835] 0811[工学-水利类] 082302[082302] 0812[工学-测绘类] 081202[081202] 0823[工学-农业工程类] 

核心收录：

D　O　I：10.3969/j.issn.0258-2724.20210656

馆 藏 号：203118125...