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

摘要：

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

关键词：列控系统、时间约束、混合通信顺序进程、时间自动机、RBC切换

所属期刊栏目：33

分类号：TP393;U283(计算技术、计算机技术)

资助基金：国家高技术研究发展计划863计划2009AA11Z221;新世纪优秀人才支持计划NCET070059

在线出版日期：2011-09-26（万方平台首次上网日期，不代表论文的发表时间）

页数：共8页

页码：54-61