- ISSN 0258-2724
- CN 51-1277/U
- EI Compendex
- Scopus
- Indexed by Core Journals of China, Chinese S&T Journal Citation Reports
- Chinese S&T Journal Citation Reports
- Chinese Science Citation Database
| Citation: | WANG Xia, WANG Keming, XU Yang, TANG Weijian. Safety Design of Level Crossing Control System Based on Formal Method[J]. Journal of Southwest Jiaotong University, 2023, 58(1): 109-116. doi: 10.3969/j.issn.0258-2724.20210656
|
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.
| [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.
|
Figures(7)
DownLoad:
