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

作者：吕继东; 唐涛

来源：铁道学报, 2011, (06): 54-61.

• 列控系统
• 时间约束
• 混合通信顺序进程
• 时间自动机
• RBC切换 train control system
• time constraints
• HCSP
• timed automaton
• RBC handover

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

• 单位
  北京交通大学; 轨道交通控制与安全国家重点实验室