运行时验证及其在列车运行控制系统中的应用

• 作者: 唐涛 徐田华 李宪 柴铭 赵林
• 来源期刊: 铁道学报
• 学科: 交通运输
• 关键词: 模型检验 测试 多值逻辑 公式重写 列车运行控制系统
• 年，卷（期）: 2011,（12）
• 所属期刊栏目: 铁道通信信号
• 页码范围: 65-71
• 分类号: U284.482
• 字数: 6845字
• 语种: 中文
• DOI: 10.3969/j.issn.1001-8360.2011.12.011

摘要

运行时验证是一种将模型检验方法与测试相结合的轻量级验证技术,它能够有效地降低系统验证的复杂度,提供系统运行阶段的安全保障,因此在安全苛求系统的验证领域有着极其重要的应用.本文提出一种基于三值逻辑的有限轨迹LTL可执行语义,允许“真”和“假”以外的逻辑值来显式的刻画验证过程中可能出现的非确定性,从而使得验证的结果更加精确.针对新的LTL语义给出了基于公式重写的运行监控算法和近似优化策略,并结合欧洲列车运行控制系统的实例,分析探讨了该方法在轨道交通控制领域的应用.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	唐涛	北京交通大学轨道交通控制与安全国家重点实验室	152	2578	27.0	40.0
2	徐田华	北京交通大学轨道交通控制与安全国家重点实验室	21	347	11.0	18.0
3	赵林	北京交通大学轨道交通控制与安全国家重点实验室	11	160	8.0	11.0
4	李宪	北京交通大学轨道交通控制与安全国家重点实验室	3	58	3.0	3.0
5	柴铭	北京交通大学轨道交通控制与安全国家重点实验室	2	12	1.0	2.0