【摘 要】
：
近年来,随着城市化进程的加速,城市轨道交通迅速发展,基于通信的列车运行控制(Communication Based Train Control,CBTC)系统逐渐被广泛使用。区域控制器(Zone Controller,ZC
论文部分内容阅读
近年来,随着城市化进程的加速,城市轨道交通迅速发展,基于通信的列车运行控制(Communication Based Train Control,CBTC)系统逐渐被广泛使用。区域控制器(Zone Controller,ZC)作为CBTC系统地面核心子系统,通过与其它设备间的交互通信,实时的为列车计算移动授权(MovementAuthority,MA)信息,实现列车的间隔控制。ZC子系统作为一个典型的实时系统,其行为状态的迁移过程中,逻辑性和时序性的正确对保障系统安全具有重要意义。因此,为了进一步确保ZC子系统能够安全运行实现其功能,本文提出了一种基于时间自动机的ZC子系统建模与验证方法,通过对系统进行建模,从逻辑性和时序性两方面验证分析系统运行时是否满足安全需求。本文首先对ZC子系统的特点进行了分析,并采用层次化结构思想把ZC子系统分为系统设备层和功能逻辑层。其次,根据UML扩展方式,针对ZC子系统特点,把顺序图元模型在时钟约束和变量两方面做了合理扩展,使其能够更充分地描述系统在交互过程中的逻辑性和时序性。然后,根据模型转化理论,在确保模型转换过程一致性的基础上,制定合理的转换规则,把半形式化扩展顺序图转化为形式化的时间自动机模型。并对形式化验证方法分类做了概述,阐述了时间自动机模型验证工具UPPAAL的基本结构和功能。在此基础上,分析了 LTL公式到BNF公式的逻辑语义转换形式。本文最后选取MA回撤和列车跨越ZC边界区域两个场景案例进行分析,分别建立时间自动机模型,并在UPPAAL软件中构造了时间自动机网络模型。通过对两个不同场景下系统需求的逻辑性和时序性验证,从逻辑性和时序性方面保证了系统的安全运行。证明了本文提出的建模和验证方法的可行性和有效性。
其他文献
在医疗体制改革背景下,医疗保险得到了全面实施,促使病案信息应用价值显著提升,并呈现较为广泛应用范围.对于病案管理人员来讲,加大病案复印重视力度,针对新时期工作面临挑战
目的:观察不同剂量的夏枯草口服液治疗乳腺增生的临床差异.方法:治疗组30例,口服夏枯草口服液一次20ml,每日两次;对照组30例,口服夏枯草口服液一次10ml,每日三次.疗程结束后
针对当前我国高校规模的进一步壮大和良好发展,在高校中各个教师早开展教育工作中,也要不断的优化和改善自身教育理念和教育思想.可是在很多院校中的财务管理中还是存在急需
随着我国社会经济的不断发展,人们生活水平逐渐提高,人们从关注小康社会,解决温饱问题转向提高自身的生活质量,尤其对身体健康方面投以广泛关注.大众对健康问题的重视,新医改
社会在进步,数字化、信息化影响着每个人的生活,冲击着每个人的岗位.本文就新形势下管理会计与财务会计结合的必要性与结合策略进行分析,希望能对我国企业的财务改革提供帮助
人体健康参数的检测对于评估人体健康状况、及早发现健康隐患有重要意义,是疾病发现、控制和治疗的前提。光纤传感器由于其体积小重量轻、可弯曲、对电磁绝缘等特性,在生物医
过江桥梁是滨江城市交通衔接的纽带，为江河两岸的人、车、物的空间移动提供了重要的通道。随着我国经济的高速发展，居民的机动车拥有量的迅猛增加，居民的交通出行也急剧增多，于是
为了满足社会经济的发展需求,事业单位不断的进行财务制度的改革和创新.于2019年1月1日起施行新的政府会计制度.新财务制度的颁布为事业单位的财务核算工作提供了指导,并为事
数据通信系统(Data Communication System,DCS)是基于通信的列车运行自动控制系统(Communications Based Train Control System,CBTC)的重要子系统之一,加强对DCS信息安全的
企业铁路主要是在企业内部承担原材料、半成品的厂内运输和成品的外发作业，是保证企业正常作业生产的重要基础设施。然而面对企业铁路运量大、作业灵活、货物种类繁多、技术作