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

摘要：

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

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

所属期刊栏目：37

分类号：U285.41(铁路通信、信号)

资助基金：国家自然科学基金资助项目No.U1534208Foundation Item:The National Natural Science Foundation of China U1534208

在线出版日期：2016-12-20（万方平台首次上网日期，不代表论文的发表时间）

页数：共7页

页码：196-202