毕业设计：文献参考（8）
一、基本信息
- 标题：城轨CBTC系统数据的安全处理与验证方法研究
- 来源：北京交通大学
- 作者：黄友能
二、研究背景
随着我国国民经济和社会的快速发展，城市化进程的加快，形成了以北京、上海、广州为代表的人口超千万的特大型城市，交通拥堵问题成为这些城市迫切需要解决的问题。轨道交通作为一个城市重要的基础设施和民生工程，是一种资源节约型和环境友好型的运输方式，已成为目前各大城市用来解决城市交通拥堵的有效手段，据中国城市轨道交通协会统计，截至2013年12月，我国城市轨道交通开通运营里程已超过2340公里，预计到2015年，我国城市轨道交通里程将超过3000公里[fll。为保障城市轨道交通安全、高效、准点的运行，列车自动控制系统作为城市轨道交通系统的“大脑和神经”，是必不可少的。
列车自动控制系统(简称为:列控系统)能有效防止线路上运行的列车“二冒一超”，实现对列车的间隔防护和速度防护，并在保证列车安全的前提下提高轨道交通的运输能力。随着通信技术、计算机技术、自动控制技术的发展，传统以轨道电路为车地传输方式的列车自动控制系统已逐渐被基于通信的列车自动控制系统(GBTC)取代。在国外，法国巴黎地铁已开通的3号线、5号线;伦敦地铁北线Highgate至High Barnet段;美国纽约地铁Canasie线、Flushing线;新加坡东北线;迪拜红线、绿线等采用的是CBTC系统;国内自2008年以来，新建和改造线路采用CBTC系统的轨道交通线路条数已达30多条线，CBTC系统目前已成为国内外城市轨道交通列车自动控制系统的首选。
CBTC系统的典型特征包括f2R}>}l:不依赖于轨道电路的列车主动定位;连续车一地双向数据通信技术;执行安全功能的车载和地面处理机。安全性是CBTC系统最重要、最基本的要求，指的是通过安全相关技术以及执行安全功能的车载和地面处理机，使列车运行间隔防护和速度防护功能实现上不存在不可接受的风险。
三、具体内容
第五章:基于形式化模型的数据安全验证方法。针对具有条件关系的静态数据验证，提出将UML建立的时序模型转换为CSP模型进行验证研究的方法，并重点研究了以UML为源模型，通过LTS语义转换以及模型转换规则，并通过实例说明模型转换方法的可行;针对动态数据验证，提出将UML建立的时序模型转换为TA模型进行验证研究的方法，并重点研究了UML扩展机制和UML时序模型到TA模型的转换规则，解决了动态数据存在的一致性问题和数据在应用过程中出现的组合错误问题，并通过实例说明模型转换方法的可行性。
四、参考文献
[1]黄友能. 城轨CBTC系统数据的安全处理与验证方法研究[D].北京交通大学,2014.