基于时间自动机的车车通信移动闭塞功能研究与验证
发布时间：2021-03-01 08:24
随着城轨CBTC（Communication Based Train Control,基于通信的列车运行控制）信号系统的发展以及5G（5th Generation Mobile Networks,第5代移动通信网络）技术的应用,基于车车通信的列车运行控制系统研究应运而生。该系统突破了传统CBTC系统以地面设备为核心的列车控制方式,重组系统架构,优化系统功能,以车载设备为核心实现移动闭塞功能,提高了列车的灵活性与智能性,同时由于地面设备的精简,使得系统间接口得到简化,控制信息直达列车,降低了系统反应时间。车载移动闭塞功能作为车车通信列控系统的核心功能,其正确性与有效性必须得到保障。形式化验证与仿真测试验证可以对系统规范制定的合理性以及系统功能实现的有效性进行验证,可及时发现系统开发过程中可能存在的不安全因素,对系统的研究和应用具有理论价值与实践意义。本文以车车通信列控系统架构为基础,重点研究实现系统车载移动闭塞功能的三大主要功能——前车识别、列车筛选以及车载移动授权生成,采用时间自动机理论和UPPAAL工具对上述功能的具体实现进行了形式化描述与验证,并在测试平台上完成了测试验证,验证了系...
【文章来源】：兰州交通大学甘肃省
【文章页数】：73 页
【学位级别】：硕士
【部分图文】：
CBTC系统子系统间接口图
基于时间自动机的车车通信移动闭塞功能研究与验证-2-(Vehicle-to-VehicleCommunicationBasedTrainControlsystem)系统应运而生，以下简称VBTC系统。VBTC系统开发的核心是简化传统系统架构，减少车站及区间设备布置，由车载来实现列控系统的大部分或全部功能，提高车载的自主性与灵活性。总体来说VBTC系统具有以下优势[3]：(1)建设投入和全生命周期成本减少。据资料显示，VBTC系统可减少约20%的设备。信号设备大多安装于列车上，维修工作得到简化且易于线路扩建与改造；(2)系统响应时间缩短，性能得到改善。通过列车间直接通信的方式减少了系统间接口，缩短了系统响应时间；(3)有利于互联互通的实施。系统对地面设备依赖减轻且车地通信接口减少，更有利于实现不同制式之间的互联互通。图1.1与图1.2分别为CBTC系统与VBTC系统的子系统间接口图。图1.1CBTC系统子系统间接口图图1.2VBTC系统子系统间接口图目前对于VBTC系统的研究尚处于开发实验阶段，典型的科研单位包括阿尔斯通、交控科技等公司。在一个新系统的开发初期，采取一定的方法对系统进行验证是非常有必要的。标准EN50129与IEC61508[4,5]均推荐使用形式化方法对完善度等级达到3级以上的系统进行验证。形式化方法以严格的数学定义对复杂实时系统的功能进行描述并建
基于时间自动机的车车通信移动闭塞功能研究与验证-12-(c)E[]p(d)A<>p(e)p→q图2.1BNF语义示意图2.4小结本章对本课题采用的基础理论与该理论对应的验证工具进行了介绍。首先对形式化验证方法的概念与特点进行了简要介绍，并对目前针对列控系统实时性建模验证的形式化方法依据的数学基储采用的验证工具以及各自的特点进行了总结，给出了本文采用时间自动机作为建模理论的缘由；其次对时间自动机理论中的相关定义与语义进行了介绍，并给出了时间自动机的积的定义；最后对建模与验证工具UPPAAL的界面组成、使用说明以及验证采用的BNF语法进行了介绍。
【参考文献】：
期刊论文
[1]浅析白盒测试在软件测试中的应用[J]. 田春竹,邢航. 中国信息化. 2019(08)
[2]关于欧盟Shift2Rail计划的研究[J]. 林鸿,王林美,魏艳萍. 国外铁道车辆. 2019(01)
[3]基于地面无联锁及区域控制器的新一代CBTC系统方案[J]. 杜恒,孙军国,张强,陈军. 都市快轨交通. 2017(04)
[4]基于通信的列车控制系统可信构造:形式化方法综述[J]. 陈铭松,鲍勇翔,孙海英,缪炜恺,陈小红,周庭梁. 软件学报. 2017(05)
[5]下一代列控系统技术方案探讨[J]. 程剑锋,田青,赵显琼,孙帝. 中国铁路. 2014(12)
[6]形式化方法在列车运行控制系统中的应用[J]. 曹源,唐涛,徐田华,穆建成. 交通运输工程学报. 2010(01)
[7]基于UPPAAL的铁路车站信号联锁系统模型验证[J]. 熊振华,魏臻. 科学技术与工程. 2008(07)
[8]仿真系统VV&A及其标准/规范研究[J]. 刘兴堂,刘力,孙文. 计算机仿真. 2006(03)
博士论文
[1]CBTC联锁系统的形式化建模与验证方法研究[D]. 于潇.中国铁道科学研究院 2017
[2]列控系统需求规范形式化建模与验证方法研究[D]. 谢雨飞.北京交通大学 2012
[3]列车运行控制系统分层形式化建模与验证分析[D]. 吕继东.北京交通大学 2011
硕士论文
[1]以车载为核心的联锁控制建模与验证研究[D]. 郑伟.北京交通大学 2019
[2]基于模型的CBTC区域控制器测试序列自动生成方法的研究[D]. 宋爽.兰州交通大学 2018
[3]CBTC区域控制子系统的建模分析与验证[D]. 杨璐.兰州交通大学 2018
[4]基于车车通信的列控系统车载子系统建模与实现[D]. 许镇.北京交通大学 2018
[5]基于SCADE的CBTC系统移动授权建模与验证[D]. 杨巧.西南交通大学 2017
[6]基于时间自动机的列控中心建模与半实物仿真[D]. 柳杨.北京交通大学 2017
[7]车—车通信技术在列控系统车载设备中的应用研究[D]. 王鹏.北京交通大学 2017
[8]基于TSSM的车车通信系统车载移动授权模块的建模和验证[D]. 何芊颖.北京交通大学 2017
[9]基于状态机的车车通信环境下列车通信协作研究[D]. 李聪.北京交通大学 2017
[10]基于资源自主调配的联锁子系统在车车通信系统中的应用[D]. 方思仪.北京交通大学 2017
本文编号：3057217
【文章来源】：兰州交通大学甘肃省
【文章页数】：73 页
【学位级别】：硕士
【部分图文】：
CBTC系统子系统间接口图
基于时间自动机的车车通信移动闭塞功能研究与验证-2-(Vehicle-to-VehicleCommunicationBasedTrainControlsystem)系统应运而生，以下简称VBTC系统。VBTC系统开发的核心是简化传统系统架构，减少车站及区间设备布置，由车载来实现列控系统的大部分或全部功能，提高车载的自主性与灵活性。总体来说VBTC系统具有以下优势[3]：(1)建设投入和全生命周期成本减少。据资料显示，VBTC系统可减少约20%的设备。信号设备大多安装于列车上，维修工作得到简化且易于线路扩建与改造；(2)系统响应时间缩短，性能得到改善。通过列车间直接通信的方式减少了系统间接口，缩短了系统响应时间；(3)有利于互联互通的实施。系统对地面设备依赖减轻且车地通信接口减少，更有利于实现不同制式之间的互联互通。图1.1与图1.2分别为CBTC系统与VBTC系统的子系统间接口图。图1.1CBTC系统子系统间接口图图1.2VBTC系统子系统间接口图目前对于VBTC系统的研究尚处于开发实验阶段，典型的科研单位包括阿尔斯通、交控科技等公司。在一个新系统的开发初期，采取一定的方法对系统进行验证是非常有必要的。标准EN50129与IEC61508[4,5]均推荐使用形式化方法对完善度等级达到3级以上的系统进行验证。形式化方法以严格的数学定义对复杂实时系统的功能进行描述并建
基于时间自动机的车车通信移动闭塞功能研究与验证-12-(c)E[]p(d)A<>p(e)p→q图2.1BNF语义示意图2.4小结本章对本课题采用的基础理论与该理论对应的验证工具进行了介绍。首先对形式化验证方法的概念与特点进行了简要介绍，并对目前针对列控系统实时性建模验证的形式化方法依据的数学基储采用的验证工具以及各自的特点进行了总结，给出了本文采用时间自动机作为建模理论的缘由；其次对时间自动机理论中的相关定义与语义进行了介绍，并给出了时间自动机的积的定义；最后对建模与验证工具UPPAAL的界面组成、使用说明以及验证采用的BNF语法进行了介绍。
【参考文献】：
期刊论文
[1]浅析白盒测试在软件测试中的应用[J]. 田春竹,邢航. 中国信息化. 2019(08)
[2]关于欧盟Shift2Rail计划的研究[J]. 林鸿,王林美,魏艳萍. 国外铁道车辆. 2019(01)
[3]基于地面无联锁及区域控制器的新一代CBTC系统方案[J]. 杜恒,孙军国,张强,陈军. 都市快轨交通. 2017(04)
[4]基于通信的列车控制系统可信构造:形式化方法综述[J]. 陈铭松,鲍勇翔,孙海英,缪炜恺,陈小红,周庭梁. 软件学报. 2017(05)
[5]下一代列控系统技术方案探讨[J]. 程剑锋,田青,赵显琼,孙帝. 中国铁路. 2014(12)
[6]形式化方法在列车运行控制系统中的应用[J]. 曹源,唐涛,徐田华,穆建成. 交通运输工程学报. 2010(01)
[7]基于UPPAAL的铁路车站信号联锁系统模型验证[J]. 熊振华,魏臻. 科学技术与工程. 2008(07)
[8]仿真系统VV&A及其标准/规范研究[J]. 刘兴堂,刘力,孙文. 计算机仿真. 2006(03)
博士论文
[1]CBTC联锁系统的形式化建模与验证方法研究[D]. 于潇.中国铁道科学研究院 2017
[2]列控系统需求规范形式化建模与验证方法研究[D]. 谢雨飞.北京交通大学 2012
[3]列车运行控制系统分层形式化建模与验证分析[D]. 吕继东.北京交通大学 2011
硕士论文
[1]以车载为核心的联锁控制建模与验证研究[D]. 郑伟.北京交通大学 2019
[2]基于模型的CBTC区域控制器测试序列自动生成方法的研究[D]. 宋爽.兰州交通大学 2018
[3]CBTC区域控制子系统的建模分析与验证[D]. 杨璐.兰州交通大学 2018
[4]基于车车通信的列控系统车载子系统建模与实现[D]. 许镇.北京交通大学 2018
[5]基于SCADE的CBTC系统移动授权建模与验证[D]. 杨巧.西南交通大学 2017
[6]基于时间自动机的列控中心建模与半实物仿真[D]. 柳杨.北京交通大学 2017
[7]车—车通信技术在列控系统车载设备中的应用研究[D]. 王鹏.北京交通大学 2017
[8]基于TSSM的车车通信系统车载移动授权模块的建模和验证[D]. 何芊颖.北京交通大学 2017
[9]基于状态机的车车通信环境下列车通信协作研究[D]. 李聪.北京交通大学 2017
[10]基于资源自主调配的联锁子系统在车车通信系统中的应用[D]. 方思仪.北京交通大学 2017
本文编号：3057217
本文链接：https://www.wllwen.com/kejilunwen/daoluqiaoliang/3057217.html
