安全计算机通信管理机制的形式化验证与实现

doi:10.11959/j.issn.1000-436x.2016237

Abstract

Abstract:

In order to improve the system compatibility of the safety computer of the next generation train operation con-trol system, first of all, the structure was analyzed and the management mechanism was designed, the state transition model of management unit was established, and the correctness of the model was verified by formal verification tools at the same time. Then the software and hardware which based on micro controller unit (MCU) were designed and imple-mented. The verification and test results show that the management mechanism design meets the design requirements, the management unit can achieve the expected state transfer function.

Key words: train control system, safety computer, communication management mechanism, formal verification

Liang LIANG,Yuan CAO,Lian-chuan MA,Yu-zhuo ZHANG,Heng-kui LI. Formal verification and implementation of safety computer communication management mechanism[J]. Journal on Communications, 2016, 37(11): 196-204.

Figures/Tables 12

References 10

[1]	郑升，曹源，张玉琢，等．通用型列控系统的安全计算机设计与验证[J]. 北京交通大学学报, 2014,38(3):128-134. ZHENG S , CAO Y , ZHANG Y Z , et al. Design and verification of general train control system's safety computer[J]. Journal of Beijing Jiaotong University, 2014,38(3):128-134.
[2]	LEE J D , BHOJWANI P S , MAHAPATRA R N . A safety analysis framework for cots microprocessors in safety-critical applications[C]// Ninth IEEE International Symposium on High-Assurance Systems Engineering. Plano, US, 2007:407-408.
[3]	芶冬荣，刘海清 . 双机容错计算机系统的设计与实现[J]. 计算机工程, 2008,34(15):255-258. GOU D R , LIU H Q . Design and implementation of dual-computer fault-tolerant system[J]. Computer engineering, 2008,34(15):255-258.
[4]	马连川，高倍力 . 一种高安全、容错控制计算机的设计与实现[J]. 中国安全科学学报, 2004,14(8):101-105. MA L C , GAO B L . Design and realization of highly safe fault tolerant control computer[J]. China Safety Science Journal, 2004,14(8):101-105.
[5]	齐志华，王海峰 . 一种嵌入式二乘二取二容错计算机联锁系统设计[J]. 北京交通大学学报, 2006,30(5):96-100. QI Z H , WANG H F . Design of an embedded double 2-vote-2 fault to-lerant computer-based interlocking system[J]. Journal of Beijing Jiao-tong University, 2006,30(5):96-100.
[6]	SCHERRER C , STEININGER A . Dealing with dormant faults in an embedded fault-tolerant computer system[J]. IEEE Transaction on Reliability, 2003,52(4):512-522.
[7]	郭志良，郜春海，马连川，等．基于时间自动机模型的安全计算机平台的形式化验证[J]. 铁道学报, 2011,33(6):68-73. GUO Z L , GAO C H , MA L C , et al. Formal verification of safety computer platform based on timed automata model[J]. Journal of the China Railway Society, 2011,33(6):68-73.
[8]	CENELEC EN50129-2006. Railway applications: safety related elec-tronic systems for signaling[S]. 2006.
[9]	EC61508-2. Functional safety of electrical/electronic/programmable electronic safety-related systems-part II[S]. 2010.
[10]	PAOLO A , ANGELO G , ELVINIA R . A model advisor for NuSMV specifications[J]. Innovations in System ＆ Software Engineering, 2011,7:97-107.

Metrics

Recommended 0

No Suggested Reading articles found!

Formal verification and implementation of safety computer communication management mechanism

RichHTML

PDF

Knowledge

Abstract

Cite this article

share this article

Figures/Tables 12

References 10

Related Articles 5

Metrics

Recommended 0

[1]	Jin ZHANG, Qiang GE, Weihai XU, Yiming JIANG, Hailong MA, Hongtao YU. Design, implementation and formal verification of BGP proxy for mimic router [J]. Journal on Communications, 2023, 44(3): 33-44.
[2]	Ying GAO,Yuan CAO,Yongkui SUN,Lianchuan MA,Chunhua HONG,Yuzhuo ZHANG. Analysis and verification of safety computer time constraints for train-to-train communications [J]. Journal on Communications, 2018, 39(12): 82-90.
[3]	Xia ZHANG,Lian-chuan MA,Yuan CAO,Yu-zhuo ZHANG. Research on data loss probability and its impact of CTCS-3 train ground communication based on GSM-R [J]. Journal on Communications, 2014, 35(12): 203-209.
[4]	. Research on data loss probability and its impact of CTCS-3 train ground communication based on GSM-R [J]. Journal on Communications, 2014, 35(12): 24-209.
[5]	Jing-jing GUI,Yu-sen ZHANG. New approach to security analysis of ad hoc routing protocols based on strand space model [J]. Journal on Communications, 2010, 31(9A): 217-222.