基于NuSMV和STPA的RBC交接场景安全分析方法研究

《基于NuSMV和STPA的RBC交接场景安全分析方法研究》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、密级：公开１０００４学校代码：：１财交私綮｜ＢＥＩＪＩＮＧＪＩＡＯＴＯＮＧＵＮＩＶＥＲＳＩＴＹ硕士学位论文基于ＮｕＳＭＶ和ＳＴＰＡ的ＲＢＣ交接场景安全分析方法研究作者姓名夏宇学科专业交通信息工程及控制指导教师王化深教授培养院系电子信息工程学院：零－八年＾１赫■Ａ妓遥乂華硕士学位论文基于ＮｕＳＭＶ和ＳＴＰＡ的ＲＢＣ交接场景安全分析方法研究ＲｅｓｅａｒｃｈｏｎＳａｆｅｔｙＡｎａｌｙｓｉｓＭｅｔｈｏｄｆｏｒＲＢＣＨａｎｄｏｖｅｒＢａｓｅｄｏｎＮｕＳＭＶａｎ

2、ｄＳＴＰＡ作者：夏宇导师：王化深教授北京交通大学２０１８年３月学位论文版权使用授权书本学位论文作者完全了解北京交通大学有关保留。、使用学位论文的规定特授权北京交通大学可以将学位论文的全部或部分内容编入有关数据库进行检索，提供阅览服务，、、汇编以供查阅和借阅并采用影印缩印或扫描等复制手段保存。同意学校向国家有关部门或机构送交论文的复印件和磁盘。学校可以为存在馆际合作关系的兄弟高校用户提供文献传递服务和交换服务。（保密的学位论文在解密后适用本授权说明）学位论文作者签名导师签名：：ｉｆ签字

3、］：日丨期丨签字減年玥丨＾１０００学校代码：４密级：公开北京交通大学硕士学位论文基于ＮｕＳＭＶ和ＳＴＰＡ的ＲＢＣ交接场景安全分析方法研究ＲｅｓｅａｒｃｈｏｎＳａｆｅｔＡｎａｌｓｉｓＭｅｔｈｏｄｆｏｒＲＢＣＨａｎｄｏｖｅｒＢａｓｅｄｏｎｙｙＮｕＳＭＶａｎｄＳＴＰＡ作者姓名：夏宇学号：１５１２０２９４导师姓名：王化深职称：教授？学位类别．工学学位级别：硕士学科专业：交通信息工程及控制研宄方向：轨道交通安全理论与方法北京交通大学２０１８年３月ｉ致谢

4、本论文的工作是在我的导师王化深教授的悉心指导下完成的，王化深教授严谨的治学态度和科学的工作方法给了我极大的帮助和影响。在此衷心感谢三年来王化深老师对我的关心和指导。刘金涛老师悉心指导我完成了实验室的科研工作，在学习上和生活上都给予了我很大的关心和帮助，对于我的科研工作和论文提出了许多的宝贵意见，在此向刘金涛老师表示衷心的谢意。、在实验室工作及撰写论文期间，李明孙心宇等同、刘苏、秦晓光、胡少强。学对我论文中的研究工作给予了热情帮助，在此向他们表达我的感激之情另外也感谢我的父亲母亲，他们的理解和支持使我能够在学校

5、专心完成我的学业。ｉｉｉ？摘要中国列车运行控制系统ｅｓｅＴｒａｎＣｏｎｔｓｔｅｍＬｅｖｅＴＣＳ－３３级（ＣｈｉｎｉｒｏｌＳｙｌ３，Ｃ）是我国高速铁路的核心装备，，负责保障高速铁路列车的行车安全也是高速铁路“”的神经中枢，其安全性对于高速铁路的安全运营起到了关键的作用。无线闭塞ＲａｄＢｌｏＢＣ－中心（ｉｏｃｋＣｅｎｔｅｒ，Ｒ）交接场景是ＣＴＣＳ３级列车运行控制系统（简称ＣＴＣＳ－３级列控系统）的重要运营场景。针对其特点研究有效的、科学的安全－分析方法，对于保障高速铁路的安全具有重

6、要意义，ＣＴＣＳ３。然而级列控系统的功能和组件交互之间的关系错综复杂，运用传统的安全分析方法时会面临挑战。－系统理论过程分析（ＳｙｓｔｅｍＴｈｅｏｒｅｔｉｃＰｒｏｃｅｓｓＡｎａｌｙｓｉｓ，ＳＴＰＡ）作为建立在系统理ｔ－Ｔｈｔ论事故模型（ＳｓｅｍｓｅｏｒｅｉｃＡｃｃｔＭＴＡＭＰｙｉｄｅｎｏｄｅｌａｎｄＰｒｏｃｅｓｓ，Ｓ）基础上的新－技术，将导致危险的主要原因归结为组件间的异常交互３，满足ＣＴＣＳ级列控系一统对安全分析方法的要求。但是，目前没有统的方法来描述该模型，而采用自然语言建模又容易受人员表述能力的影响

7、而导致歧义，ＳＴＰＡ。此外安全分析主要依靠分析人员人工实施，其分析结果的可信度受分析人员经验的影响较大。一本论文从目前现有的建模与分析方法存在的不足出发，利用ＵＭＬ统建模语言的可扩展性等优点，对ＳＴＰＡ方法中系统分层控制结构模型的构建方法进行改进，并利用ＮｕＳＭＶ能自动给出反例的特性辅助实施ＳＴＰＡ安全分析过程。主要的内容包括：（１）在理解并阅读了大量国内外文献研宄之后，简单介绍目前安全分析方法的研宄情况，并针对不同安全分析方法的优点及不足做出对比和分析，明确现有安全分析方法在列控领域的研究前景。（２）设

8、计面向ＳＴＡＭＰ模型的ＵＭＬ概要文件，扩展ＵＭＬ类图和控制反馈消息，针对ＳＴＰＡ方法进行扩展。，从而刻画出待分析系统的分层控制结构模型（３）将上述半形式化的ＵＭＬ模型转化