Formal verification and implementation of safety computer communication management mechanism

Liang LIANG; Yuan CAO; Lian-chuan MA; Yu-zhuo ZHANG; Heng-kui LI

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

您当前的位置：

首页 >

文章列表页 >

Formal verification and implementation of safety computer communication management mechanism

Academic communication | 更新时间：2024-06-05

- Formal verification and implementation of safety computer communication management mechanism
- Journal on Communications Vol. 37, Issue 11, Pages: 196-204(2016)
- 作者机构：
  
  1. 北京交通大学电子信息工程学院，北京 100044
  2. 北京交通大学轨道交通运行控制系统国家工程研究中心，北京 100044
  3. 中车青岛四方机车车辆股份有限公司，山东青岛 266111
- 作者简介：
- 基金信息：
  
  The National Natural Science Foundation of China(U1534208)
- DOI：10.11959/j.issn.1000-436x.2016237
  CLC： U285.41
- Online First：2016-11，
  
  Published：25 November 2016
- 稿件说明：
移动端阅览
Liang LIANG, Yuan CAO, Lian-chuan MA, et al. Formal verification and implementation of safety computer communication management mechanism[J]. Journal on Communications, 2016, 37(11): 196-204.
DOI：

Liang LIANG, Yuan CAO, Lian-chuan MA, et al. Formal verification and implementation of safety computer communication management mechanism[J]. Journal on Communications, 2016, 37(11): 196-204. DOI： 10.11959/j.issn.1000-436x.2016237.

摘要

为提高下一代列车运行控制（简称列控）系统安全计算机的系统兼容性，首先对其结构进行简要分析，并对管理机制进行设计，建立了管理单元状态转移模型，同时以形式化验证工具对模型的正确性进行了验证。在此基础上对基于微控制单元(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.

关键词

Keywords

references

郑升，曹源，张玉琢，等．通用型列控系统的安全计算机设计与验证 [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 .

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 .

芶冬荣，刘海清 . 双机容错计算机系统的设计与实现 [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 .

马连川，高倍力 . 一种高安全、容错控制计算机的设计与实现 [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 .

齐志华，王海峰 . 一种嵌入式二乘二取二容错计算机联锁系统设计 [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 .

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 .

郭志良，郜春海，马连川，等．基于时间自动机模型的安全计算机平台的形式化验证 [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 .

CENELEC EN50129-2006 . Railway applications: safety related elec-tronic systems for signaling [S ] . 2006 .

EC61508-2 . Functional safety of electrical/electronic/programmable electronic safety-related systems-part II [S ] . 2010 .

PAOLO A , ANGELO G , ELVINIA R . A model advisor for NuSMV specifications [J ] . Innovations in System ＆ Software Engineering , 2011 , 7 : 97 - 107 .

Views

1517

下载量

CSCD

Alert me when the article has been cited

提交

Tools

Publicity Resources

Formal verification of a concurrent file system based on lock guarantee conditions extended concurrent separation logic

Design, implementation and formal verification of BGP proxy for mimic router

Analysis and verification of safety computer time constraints for train-to-train communications

Related Author

LI Wenbo

YANG Qiusong

LI Mingshu

ZHENG Xinmin

Qiang GE

Hongtao YU

Hailong MA

Yiming JIANG

Related Institution

National Engineering Research Center of Fundamental Software (Institute of Software, Chinese Academy of Sciences)

University of Chinese Academy of Sciences

The Endogenous Security Research Centre, Purple Mountain Laboratories

School of Cyber Science and Engineering, Southeast University

Institute of Information Technology, Information Engineering University

AI问答

⁰