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

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

通信学报 ›› 2016, Vol. 37 ›› Issue (11): 196-204.doi: 10.11959/j.issn.1000-436x.2016237

• 学术通信 • 上一篇

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

梁靓¹,曹源²(),马连川²,张玉琢²,李恒奎³

¹ 北京交通大学电子信息工程学院，北京 100044
² 北京交通大学轨道交通运行控制系统国家工程研究中心，北京 100044
³ 中车青岛四方机车车辆股份有限公司，山东青岛 266111

出版日期:2016-11-25 发布日期:2016-11-30
基金资助:
国家自然科学基金资助项目

Formal verification and implementation of safety computer communication management mechanism

Liang LIANG¹,Yuan CAO²(),Lian-chuan MA²,Yu-zhuo ZHANG²,Heng-kui LI³

¹ School of Electronic and Information Engineering, Beijing Jiaotong University, Beijing 100044, China
² National Engineering Research Center of Rail Traffic Control System, Beijing Jiaotong University, Beijing 100044, China
³ CRCC Qingdao Sifang Co., Ltd., Qingdao 266111, China

Online:2016-11-25 Published:2016-11-30
Supported by:
The National Natural Science Foundation of China

摘要/Abstract

摘要：

为提高下一代列车运行控制（简称列控）系统安全计算机的系统兼容性，首先对其结构进行简要分析，并对管理机制进行设计，建立了管理单元状态转移模型，同时以形式化验证工具对模型的正确性进行了验证。在此基础上对基于微控制单元(MCU, micro controller unit)的管理单元进行了软硬件的设计实现与测试。验证和测试结果表明，所设计的管理机制符合设计规范的要求，管理单元能够实现预期的状态转移功能。

关键词: 列控系统, 安全计算机, 通信管理机制, 形式化验证

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

梁靓,曹源,马连川,张玉琢,李恒奎. 安全计算机通信管理机制的形式化验证与实现[J]. 通信学报, 2016, 37(11): 196-204.

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.

图/表 12

图1

图2

图3

图4

图5

图6

图7

图8

图9

图10

图11

图12

参考文献 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.

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

Formal verification and implementation of safety computer communication management mechanism

在线阅读

PDF下载

可视化

被引次数

摘要/Abstract

引用本文

使用本文

图/表 12

参考文献 10

相关文章 5

Metrics

推荐阅读 0

[1]	张进, 葛强, 徐伟海, 江逸茗, 马海龙, 于洪涛. 拟态路由器BGP代理的设计实现与形式化验证[J]. 通信学报, 2023, 44(3): 33-44.
[2]	高莺,曹源,孙永奎,马连川,洪春华,张玉琢. 面向车车通信的安全计算机时间约束性分析验证[J]. 通信学报, 2018, 39(12): 82-90.
[3]	张霞,马连川,曹源,张玉琢. CTCS-3级GSM-R车地通信数据丢失概率及其影响的研究[J]. 通信学报, 2014, 35(12): 203-209.
[4]	张霞，马连川，曹源，张玉琢. CTCS-3级GSM-R车地通信数据丢失概率及其影响的研究[J]. 通信学报, 2014, 35(12): 24-209.
[5]	桂荆京,张毓森. 基于串空间的ad hoc路由协议安全性分析新方法[J]. 通信学报, 2010, 31(9A): 217-222.