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

梁靓; 曹源; 马连川; 张玉琢; 李恒奎

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

您当前的位置：

首页 >

文章列表页 >

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

学术通信 | 更新时间：2024-06-05

- 安全计算机通信管理机制的形式化验证与实现
- Formal verification and implementation of safety computer communication management mechanism
- 通信学报 2016年37卷第11期页码：196-204
- 作者机构：
  
  1. 北京交通大学电子信息工程学院，北京 100044
  2. 北京交通大学轨道交通运行控制系统国家工程研究中心，北京 100044
  3. 中车青岛四方机车车辆股份有限公司，山东青岛 266111
- 作者简介：
  
  [ "梁靓（1987-），女，内蒙古赤峰人，北京交通大学硕士生，主要研究方向为列控系统安全计算机技术。" ]
  [ "曹源（1982-），男，回族，河南开封人，博士，北京交通大学副教授，主要研究方向为高速铁路通信技术。" ]
  [ "马连川（1970-），男，河北唐山人，北京交通大学副教授，主要研究方向为列控系统安全计算机技术。" ]
  [ "张玉琢（1990-），男，河南信阳人，北京交通大学博士生，主要研究方向为形式化建模与验证。" ]
  [ "李恒奎（1977-），男，山东肥城人，中车青岛四方机车车辆股份有限公司高级工程师，主要研究方向为高速动车组及地铁车辆设计。" ]
- 基金信息：
  
  国家自然科学基金资助项目(U1534208)
- DOI：10.11959/j.issn.1000-436x.2016237
  中图分类号： U285.41
- 网络首发：2016-11，
  
  纸质出版：2016-11-25
- 稿件说明：
移动端阅览
梁靓, 曹源, 马连川, 等. 安全计算机通信管理机制的形式化验证与实现[J]. 通信学报, 2016,37(11):196-204.

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.
梁靓, 曹源, 马连川, 等. 安全计算机通信管理机制的形式化验证与实现[J]. 通信学报, 2016,37(11):196-204. DOI： 10.11959/j.issn.1000-436x.2016237.

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 .

浏览量

1517

下载量

CSCD

文章被引用时，请邮件提醒。

提交

工具集

关联资源

基于锁保证条件扩展并发分离逻辑的并发文件系统形式化验证

拟态路由器BGP代理的设计实现与形式化验证

面向车车通信的安全计算机时间约束性分析验证