高速铁路列控系统运营场景实时性的建模与验证

• 作者: 吕继东 唐涛
• 来源期刊: 铁道学报
• 学科: 交通运输
• 关键词: 列控系统 时间约束 混合通信顺序进程 时间自动机 RBC切换
• 年，卷（期）: 2011,（6）
• 所属期刊栏目: 铁道通信信号
• 页码范围: 54-61
• 分类号: TP393|U283
• 字数: 4446字
• 语种: 中文
• DOI: 10.3969/j.issn.1001-8360.2011.06.010

摘要

高速铁路列控系统是一个典型的分布式实时系统,其时间约束主要反映在运营场景中子系统之间的交互过程中.时序逻辑的扩展方法并不能完全满足描述分布式实时系统性质的需要,并且随着系统的复杂性提高,列控系统运营场景中诸如超时、期限、直到…才等形式化描述与验证上存在不足.本文提出一种适合于列控系统场景建模与验证的方法,其核心思想是使用混合通信顺序进程HCSP(Hybrid Communicating Sequential Process)形式化描述分布式实时系统模型,提出转换规则,转换成时间自动机网络模型并进行自动验证.最后通过对典型场景无线闭塞中心RBC(Radio Block Center)切换的相关属性进行建模与验证,分析证明方法的有效性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	唐涛	北京交通大学轨道交通控制与安全国家重点实验室	152	2578	27.0	40.0
2	吕继东	北京交通大学轨道交通控制与安全国家重点实验室	25	310	9.0	17.0