基于UPPAAL的城市轨道交通CBTC区域控制子系统建模与验证

来源 :铁道学报 | 被引量 : 0次 | 上传用户:RS2322ABC
下载到本地 , 更方便阅读
声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架
论文部分内容阅读
CBTC(Communication Based Train Control)系统可有效提高轨道交通的列车运营效率,降低系统建设和维护费用.在系统研发过程中需对系统进行建模、仿真和验证,发现系统设计缺陷,以保证系统的安全性.CBTC区域控制子系统是一实时控制系统,它要求控制时间的精确性和控制过程的准确性.本文通过分析城市轨道交通CBTC区域控制子系统的结构,给出满足该子系统安全性的功能和性能要求,并结合时间自动机理论方法提出包含列车、速度距离控制器、区域控制器和多车控制队列的时间自动机网络模型.同时,应用UPPAAL验证工具对CBTC区域控制子系统进行仿真建模,并验证该子系统功能和性能要求,从而保证了系统模型的安全性和受限活性.
其他文献
利用自行设计的"教师实施自主学习的教学现状调查问卷",从教师对转变学生学习方式的态度及看法、教师评估自身的教学行为、教师在课堂上实践自主学习的教学状况和教师探索自
本文在回顾学界相关研究的基础上,总结“了2”的句法意义和语法意义;在语用学理论指导下,结合语料,揭示其语用意义。笔者认为,“了2”可以使交际中话语语气缓和,更加具有商榷
中介语是学习者在第二语言习得中形成的动态语言系统,是目的语的变异之一.中介语产生的因素可以分为语言内部因素和语言外部因素,主体因素和非主体因素,在线因素和社会文化因
汉语字词典字条的义项和其下辖的词条的义项间的对应关系存在三种不同的情况:一是字条义项多,字条下辖的词条的义项少;二是字条义项少,字条下辖的词条的义项多;三是字条义项
网络学习社区作为一种新型学习方式越来越被人们所接受,已经成为辅助传统课堂教学的主流应用模式.文章以Ning.com网络学习社区辅助英语写作教学为实例,介绍如何把学生的写作
反事实(counterfactual)的本质意思是指在实际生活中,某些情况并未发生,即与"事实"相反.在哲学和统计学界,有很多学者就是借用这个问题来探索事物发生的原因.笔者曾将"counte
比较研究满语方位词词缀-si和方向格词级-ci的语音形式和语法功能就会发现,二者语音对应、语义相通,具有同源关系,是由原始满一通古斯语中表达位置、方向的词缀*-tu演变而来
从仿真实验角度对支持向量机弹道识别方法的精度作进一步的分析和讨论.首先分析导致样本错分的原因,随后分别详细讨论样本数目、采样间隔和雷达噪声对识别精度的影响,得到一
利用土壤水分/圆锥指数复合测量装置,应用精细农作技术体系网格定点测量与GPS定位,在一块面积约1.27 hm2的草地上获取了土壤含水率与坚实度空间分布基础数据,并针对采样过程中出现的数据缺失,用偏最小二乘法对数据进行修补。然后运用克里格插值法进行数字化成图,并在此基础上分别对含水率与坚实度的空间变异性及两者的相关性做了分析。
为发展高功率脉冲电源的工业应用而提高其重复工作频率并实现紧凑一体化,设计了一种基于等离子体断路开关(POS)的功率脉冲电源。该电源采用LCC谐振的有源充电器,以产生初级脉