基于Timed RAISE的高速列车RBC切换协议形式化建模及验证

• 作者: 徐世泽 肖蒙
• 来源期刊: 铁道标准设计
• 学科: 工学
• 关键词: 列控系统 形式化方法 RBC切换协议 正确性与实时性
• 年，卷（期）: 2015,（6）
• 所属期刊栏目: 通信/信号
• 页码范围: 138-142,143
• 页数: 6页
• 分类号: TP301.2
• 字数: 4895字
• 语种: 中文
• DOI: 10.13238/j.issn.1004-2954.2015.06.031

摘要

在CTCS-3(Chinese Train Control System Level 3)级列控系统中,RBC(Radio Block Center)切换是影响列车安全高效运行的重要环节,现阶段对RBC切换协议进行验证分析所使用的形式化方法还存在状态爆炸或描述性质单一等问题。基于Timed RAISE的形式化方法,结合域的模型,在对RBC切换流程分析的基础上,构建状态转移图,得到切换协议的形式化模型,使用等价和推断的推理规则对模型的正确性和实时性进行推理验证,得到的结果表明,RBC切换协议满足规范标准对正确性与实时性的要求,将验证结果与其他文献的结论进行比较分析,说明该方法具有通用性,对于推广其在列控系统场景验证中的应用有一定的实际意义。

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	肖蒙	兰州交通大学自动化与电气工程学院	19	181	7.0	12.0
2	徐世泽	兰州交通大学自动化与电气工程学院	1	7	1.0	1.0