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

王霞; 王恪铭; 徐扬; 唐伟健

doi:10.3969/j.issn.0258-2724.20210656

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

doi: 10.3969/j.issn.0258-2724.20210656

王霞^{1, 2,},
王恪铭^{1, 2},
徐扬^{2, 3, ,},
唐伟健^{2, 4}

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

基金项目: 国家自然科学基金（61976130，61673320）；四川省科技计划（2022NSFSC0464)

详细信息

作者简介:
王霞（1994—），女，博士研究生，研究方向为形式化方法、模型检测，E-mail：Kelly_Wang@my.swjtu.edu.cn

通讯作者:
徐扬（1956—），男，教授，博士，研究方向为自动推理、定理证明，E-mail： xuyang@swjtu.edu.cn

中图分类号: TP301.1；U284.3
计量
- 文章访问数: 420
- HTML全文浏览量: 231
- PDF下载量: 33
- 被引次数: 0
出版历程
- 收稿日期: 2021-08-16
- 修回日期: 2022-03-15
- 网络出版日期: 2022-11-04
- 刊出日期: 2022-04-01

Safety Design of Level Crossing Control System Based on Formal Method

WANG Xia^{1, 2
,},
WANG Keming^{1, 2},
XU Yang^{2, 3
, ,},
TANG Weijian^{2, 4}

1.
School of Computing and Artificial Intelligence, Southwest Jiaotong University, Chengdu 610031, China
2.
National-Local Joint Engineering Laboratory of System Credibility Automatic Verification, Southwest Jiaotong University, Chengdu 610031, China
3.
School of Mathematics, Southwest Jiaotong University, Chengdu 610031, China
4.
School of Information Science and Technology, Southwest Jiaotong University, Chengdu 610031, China

摘要

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

HTML全文

图 1 铁路道口控制系统的传统工作流程

Figure 1. Workflow in a traditional RLC control system

下载: 全尺寸图片幻灯片

图 2 ACS系统工作示意

Figure 2. Working diagram of ACS system

下载: 全尺寸图片幻灯片

图 3 双线双向道口传感器设置示意

Figure 3. Schematic of sensor setting for double track bi-direction RLC

下载: 全尺寸图片幻灯片

图 4 ACS系统的作业流程

Figure 4. Workflow of ACS system

下载: 全尺寸图片幻灯片

图 5 入口防护门关闭事件

Figure 5. Event of entrance barriers closed

下载: 全尺寸图片幻灯片

图 6 Animation中的部分示意

Figure 6. Oeration example in Animation

下载: 全尺寸图片幻灯片

图 7 证明义务数据统计

Figure 7. Statistic of proof obligations

下载: 全尺寸图片幻灯片

参考文献(11)

[1]	LIU B S, GHAZEL M, TOGUYÉNI A. Model-based diagnosis of multi-track level crossing plants[J]. IEEE Transactions on Intelligent Transportation Systems, 2016, 17(2): 546-556. doi: 10.1109/TITS.2015.2478910
[2]	JONSSON L, BJÖRKLUND G, ISACSSON G. Marginal costs for railway level crossing accidents in Sweden[J]. Transport Policy, 2019, 83: 68-79. doi: 10.1016/j.tranpol.2019.09.004
[3]	GHAZEL M, EL-KOURSI E M. Two-half-barrier level crossings versus four-half-barrier level crossings: a comparative risk analysis study[J]. IEEE Transactions on Intelligent Transportation Systems, 2014, 15(3): 1123-1133. doi: 10.1109/TITS.2013.2294874
[4]	曹源,唐涛,罗丹,等. 列车运行控制系统设计正确性的验证方法[J]. 西南交通大学学报,2010,45(4): 86-91. doi: 10.3969/j.issn.0258-2724.2010.04.015 CAO Yuan, TANG Tao, LUO Dan, et al. Method for verifying the correctness of train control system design[J]. Journal of Southwest Jiaotong University, 2010, 45(4): 86-91. doi: 10.3969/j.issn.0258-2724.2010.04.015
[5]	MEKKI A, GHAZEL M, TOGUYENI A. Validation of a new functional design of automatic protection systems at level crossings with model-checking techniques[J]. IEEE Transactions on Intelligent Transportation Systems, 2012, 13(2): 714-723. doi: 10.1109/TITS.2011.2178238
[6]	王恪铭,王峥. 基于形式化方法的道口控制系统规范建模与验证[J]. 西南交通大学学报,2019,54(3): 573-578,603. WANG Keming, WANG Zheng. Modeling and verification of control system specification for railway level crossings based on formal method[J]. Journal of Southwest Jiaotong University, 2019, 54(3): 573-578,603.
[7]	王霞,刘宁,王恪铭. 道口管理系统多参数的形式化建模与验证[J]. 综合运输,2019,41(2): 65-72. WANG Xia, LIU Ning, WANG Keming. Formal modeling and verification of multi-parameter model of level crossing management system[J]. China Transportation Review, 2019, 41(2): 65-72.
[8]	ABRIAL J R. Modeling in Event-B: system and software engineering [M]. Cambridge: Cambridge University Press, 2010
[9]	王恪铭,王霞,程鹏,等. 车站联锁系统行为验证与数据确认的形式化方法[J]. 西南交通大学学报,2021,56(3): 587-593,613. WANG Keming, WANG Xia, CHENG Peng, et al. Formal method for behavior verification and data validation of station interlocking system[J]. Journal of Southwest Jiaotong University, 2021, 56(3): 587-593,613.
[10]	柏卓彤,柏赟,李佳杰,等. 基于制动距离表的高速铁路ATP常用制动曲线研究[J]. 铁道标准设计,2018,62(11): 139-143,149. doi: 10.13238/j.issn.1004-2954.201712310002 BAI Zhuotong, BAI Yun, LI Jiajie, et al. The research on automatic train protection service braking curve based on braking distance table[J]. Railway Standard Design, 2018, 62(11): 139-143,149. doi: 10.13238/j.issn.1004-2954.201712310002
[11]	BÖRGER E. The ASM refinement method[J]. Formal Aspects of Computing, 2003, 15(2/3): 237-257.