基于XML的时间自动机状态可达性分析在RBC子系统中的应用

• 作者: 吕继东 唐涛 宋海锋 李开成
• 来源期刊: 铁路计算机应用
• 学科: 交通运输
• 关键词: 模型检验 CTCS-3 可达性分析 形式化建模 测试分析
• 年，卷（期）: 2014,（6）
• 所属期刊栏目: 研究与开发
• 页码范围: 10-15
• 页数: 6页
• 分类号: U284.4|TP39
• 字数: 4837字
• 语种: 中文

摘要

时间自动机中的状态可达性分析是模型建立完成之后的一个重要验证工作,大多数时间自动机建模工具均为非开源代码,不能与实际系统进行有机的结合.本文以CTCS-3中的无线闭塞中心(RBC)[1]为实际系统,提出基于XML的时间自动机状态可达性分析[2],实现了建模工具与实际测试平台不同开发环境下的数据交互,为完善整个测试平台在理论方法与实际应用相结合方面提出一个较为可行的方法.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	唐涛	北京交通大学轨道交通控制与安全国家重点实验室	152	2578	27.0	40.0
2	李开成	北京交通大学轨道交通运行控制系统国家工程研究中心	49	532	14.0	21.0
3	吕继东	北京交通大学轨道交通运行控制系统国家工程研究中心	25	310	9.0	17.0
4	宋海锋	北京交通大学轨道交通运行控制系统国家工程研究中心	3	9	2.0	3.0