基于时间自动机模型的安全计算机平台的形式化验证

• 作者: 吕继东 郜春海 郭志良 马连川
• 来源期刊: 铁道学报
• 学科: 工学
• 关键词: 实时系统 安全计算机 时间自动机 模型验证 UPPAAL
• 年，卷（期）: 2011,（6）
• 所属期刊栏目: 铁道通信信号
• 页码范围: 68-73
• 分类号: TP301.1|TP319
• 字数: 4538字
• 语种: 中文
• DOI: 10.3969/j.issn.1001-8360.2011.06.012

摘要

众多工业控制领域要求计算机控制系统具有高可靠、高可用和高安全的运行基础,2乘2取2冗余结构的安全计算机平台是提高系统安全性、可靠性的一种重要解决方式.CBTC列控系统的安全计算机平台采用2乘2取2冗余结构,它是一个实时系统,控制过程需要考虑时间因素.本文分析CBTC系统安全计算机平台系统的组成结构,提取出系统的功能约束,采用基于时间自动机理论的建模验证工具UPPAAL建立系统的自动机网络模型,进行仿真分析,验证系统的功能性、实时性、安全性要求.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	郜春海	北京交通大学轨道交通控制与安全国家重点实验室	24	761	15.0	24.0
2	吕继东	北京交通大学轨道交通控制与安全国家重点实验室	25	310	9.0	17.0
6	马连川	北京交通大学电子信息工程学院	41	300	10.0	16.0
7	郭志良	北京交通大学轨道交通控制与安全国家重点实验室	2	5	1.0	2.0