基于TRSL的RBC等级转换场景研究

• 作者: 丁春平 陈永刚
• 来源期刊: 铁道标准设计
• 学科: 交通运输
• 关键词: 列车运行控制系统 RBC等级转换 TRSL 场景切换正确性
• 年，卷（期）: 2016,（8）
• 所属期刊栏目: 通信/信号
• 页码范围: 122-129
• 页数: 8页
• 分类号: U284.48
• 字数: 6803字
• 语种: 中文

摘要

无线闭塞中心等级转换场景作为中国列车运行控制系统主要场景之一,切换成功与否直接影响高速列车的安全和运行效率。通过对形式化验证方法的分析,采用基于定理证明的时间化工业软件工程规范语言的严格方法( Timed Rigorous Approach to Industrial Software Engineering Specification Language,TRSL),在对等级转换过程进行分析的基础上,设计交互信息图,构建状态迁移图,并结合域建模方法实现对该场景的TRSL描述,最后利用语言推理规则,结合系统特性,实现对切换正确性和实时性的双重验证,结果表明：该场景满足系统规范对功能性和实时性的要求,继而说明该方法的有效性、正确性和通用性,为我国列控系统的设计开发和验证提供一种新的途径和依据。

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	陈永刚	兰州交通大学自动化与电气工程学院	50	213	8.0	11.0
2	丁春平	兰州交通大学自动化与电气工程学院	2	5	2.0	2.0