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

• 作者: 张玉琢 曹源 李恒奎 梁靓 马连川
• 来源期刊: 通信学报
• 学科: 交通运输
• 关键词: 列控系统 安全计算机 通信管理机制 形式化验证
• 年，卷（期）: 2016,（11）
• 所属期刊栏目: 学术通信
• 页码范围: 196-202
• 页数: 7页
• 分类号: U285.41
• 字数: 4493字
• 语种: 中文
• DOI: 10.11959/j.issn.1000-436x.2016237

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	马连川	北京交通大学轨道交通运行控制系统国家工程研究中心	41	300	10.0	16.0
2	张玉琢	北京交通大学轨道交通运行控制系统国家工程研究中心	21	179	8.0	13.0
3	曹源	北京交通大学轨道交通运行控制系统国家工程研究中心	62	405	10.0	18.0
4	李恒奎		10	17	2.0	4.0
5	梁靓	北京交通大学电子信息工程学院	1	10	1.0	1.0